While I can see the argument for going with uniqueness, I have to question the utility in making it a biconditional, since it's so obvious (and quick to show) in that case that the consequent implies the antecedent.
I probably won't go with anything that implies a function, since the fact that it's not syntactically a function is ultimately what made this fact unwieldy enough to split off in the first place. On Tuesday, October 22, 2019 at 8:28:53 AM UTC-4, Mario Carneiro wrote: > > 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] <javascript:>> > 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] <javascript:>. >> 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/15d87e9e-d0c0-4ff7-8ee0-e94191e754a5%40googlegroups.com.
