So while working on one of my lemmata for something else, I realized I would need something like this statement seven times (y allowed in C):
( ( A e. Fin /\ A ~~ B ) -> ( A. x e. A E. y e. B x = C -> A. x e. A E* y e. B x = C ) ) And that this might be useful elsewhere, so I decided to take it out of my naming scheme, but the best I can come up with is "finenralrexinvrmo," which seems a bit much. I guess it could be considered a version of the pigeonhole principle, if you squint...? (And yes, I realize that the restriction on the universal in the consequent is unnecessary, but the only way I could work out to prove that has this as an intermediate step, and it's relatively easy from there, so I figured it was best left here.) -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/14bfeb75-89ca-48aa-a3a5-101175e82127%40googlegroups.com.
