if you make the RHS a E!, then you can also make it a biconditional, which I think is nicer here. It's starting to look a lot like the pigeonhole principle now; there's a little group of these facts around php3 or so and you could crib the name from one of them.
Mario On Tue, Oct 22, 2019 at 8:02 AM Benoit <[email protected]> wrote: > ( ( 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 ) ) >> > > I think this lemma is natural enough to be in the main part of set.mm. I > would replace E* with E! : it strengthens the result, and more importantly, > E! is standard throughout mathematics, whereas E* is not. The way I view it > is to consider C as a function of y, and then it says: if a function > between two equinumerous finite sets is surjective, then it is bijective. > So maybe ~ finsurjbij ? > > Benoît > > -- > 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/b3fe812d-ffbc-4c76-986a-d235736fe210%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/b3fe812d-ffbc-4c76-986a-d235736fe210%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSsusnVpCV-5YgsPJBhvGvP9ELCgWD82eyE95C-j_Ojbyw%40mail.gmail.com.
