> ( ( 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.
