Metamath Proof Explorer


Theorem f1finf1o

Description: Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010) (Revised by Mario Carneiro, 27-Feb-2014) Avoid ax-pow . (Revised by BTernaryTau, 4-Jan-2025)

Ref Expression
Assertion f1finf1o A B B Fin F : A 1-1 B F : A 1-1 onto B

Proof

Step Hyp Ref Expression
1 simpr A B B Fin F : A 1-1 B F : A 1-1 B
2 f1f F : A 1-1 B F : A B
3 2 adantl A B B Fin F : A 1-1 B F : A B
4 3 ffnd A B B Fin F : A 1-1 B F Fn A
5 simpll A B B Fin F : A 1-1 B A B
6 3 frnd A B B Fin F : A 1-1 B ran F B
7 df-pss ran F B ran F B ran F B
8 7 baib ran F B ran F B ran F B
9 6 8 syl A B B Fin F : A 1-1 B ran F B ran F B
10 php3 B Fin ran F B ran F B
11 10 ex B Fin ran F B ran F B
12 11 ad2antlr A B B Fin F : A 1-1 B ran F B ran F B
13 enfii B Fin A B A Fin
14 13 ancoms A B B Fin A Fin
15 f1f1orn F : A 1-1 B F : A 1-1 onto ran F
16 f1oenfi A Fin F : A 1-1 onto ran F A ran F
17 14 15 16 syl2an A B B Fin F : A 1-1 B A ran F
18 endom A ran F A ran F
19 domsdomtrfi A Fin A ran F ran F B A B
20 18 19 syl3an2 A Fin A ran F ran F B A B
21 20 3expia A Fin A ran F ran F B A B
22 14 17 21 syl2an2r A B B Fin F : A 1-1 B ran F B A B
23 12 22 syld A B B Fin F : A 1-1 B ran F B A B
24 sdomnen A B ¬ A B
25 23 24 syl6 A B B Fin F : A 1-1 B ran F B ¬ A B
26 9 25 sylbird A B B Fin F : A 1-1 B ran F B ¬ A B
27 26 necon4ad A B B Fin F : A 1-1 B A B ran F = B
28 5 27 mpd A B B Fin F : A 1-1 B ran F = B
29 df-fo F : A onto B F Fn A ran F = B
30 4 28 29 sylanbrc A B B Fin F : A 1-1 B F : A onto B
31 df-f1o F : A 1-1 onto B F : A 1-1 B F : A onto B
32 1 30 31 sylanbrc A B B Fin F : A 1-1 B F : A 1-1 onto B
33 32 ex A B B Fin F : A 1-1 B F : A 1-1 onto B
34 f1of1 F : A 1-1 onto B F : A 1-1 B
35 33 34 impbid1 A B B Fin F : A 1-1 B F : A 1-1 onto B