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)

Ref Expression
Assertion f1finf1o ABBFinF:A1-1BF:A1-1 ontoB

Proof

Step Hyp Ref Expression
1 simpr ABBFinF:A1-1BF:A1-1B
2 f1f F:A1-1BF:AB
3 2 adantl ABBFinF:A1-1BF:AB
4 3 ffnd ABBFinF:A1-1BFFnA
5 simpll ABBFinF:A1-1BAB
6 3 frnd ABBFinF:A1-1BranFB
7 df-pss ranFBranFBranFB
8 7 baib ranFBranFBranFB
9 6 8 syl ABBFinF:A1-1BranFBranFB
10 simplr ABBFinF:A1-1BBFin
11 relen Rel
12 11 brrelex1i ABAV
13 5 12 syl ABBFinF:A1-1BAV
14 10 13 elmapd ABBFinF:A1-1BFBAF:AB
15 3 14 mpbird ABBFinF:A1-1BFBA
16 f1f1orn F:A1-1BF:A1-1 ontoranF
17 16 adantl ABBFinF:A1-1BF:A1-1 ontoranF
18 f1oen3g FBAF:A1-1 ontoranFAranF
19 15 17 18 syl2anc ABBFinF:A1-1BAranF
20 php3 BFinranFBranFB
21 20 ex BFinranFBranFB
22 10 21 syl ABBFinF:A1-1BranFBranFB
23 ensdomtr AranFranFBAB
24 19 22 23 syl6an ABBFinF:A1-1BranFBAB
25 sdomnen AB¬AB
26 24 25 syl6 ABBFinF:A1-1BranFB¬AB
27 9 26 sylbird ABBFinF:A1-1BranFB¬AB
28 27 necon4ad ABBFinF:A1-1BABranF=B
29 5 28 mpd ABBFinF:A1-1BranF=B
30 df-fo F:AontoBFFnAranF=B
31 4 29 30 sylanbrc ABBFinF:A1-1BF:AontoB
32 df-f1o F:A1-1 ontoBF:A1-1BF:AontoB
33 1 31 32 sylanbrc ABBFinF:A1-1BF:A1-1 ontoB
34 33 ex ABBFinF:A1-1BF:A1-1 ontoB
35 f1of1 F:A1-1 ontoBF:A1-1B
36 34 35 impbid1 ABBFinF:A1-1BF:A1-1 ontoB