Metamath Proof Explorer

Theorem fofinf1o

Description: Any surjection from one finite set to another of equal size must be a bijection. (Contributed by Mario Carneiro, 19-Aug-2014)

Ref Expression
Assertion fofinf1o 
|- ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) -> F : A -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) -> F : A -onto-> B )
2 fof 
 |-  ( F : A -onto-> B -> F : A --> B )
3 1 2 syl 
 |-  ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) -> F : A --> B )
4 domnsym 
 |-  ( B ~<_ ( A \ { y } ) -> -. ( A \ { y } ) ~< B )
5 simp3 
 |-  ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) -> B e. Fin )
6 simp2 
 |-  ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) -> A ~~ B )
7 enfii 
 |-  ( ( B e. Fin /\ A ~~ B ) -> A e. Fin )
8 5 6 7 syl2anc 
 |-  ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) -> A e. Fin )
9 8 ad2antrr 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> A e. Fin )
10 difssd 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( A \ { y } ) C_ A )
11 simplrr 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> y e. A )
12 neldifsn 
 |-  -. y e. ( A \ { y } )
13 nelne1 
 |-  ( ( y e. A /\ -. y e. ( A \ { y } ) ) -> A =/= ( A \ { y } ) )
14 11 12 13 sylancl 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> A =/= ( A \ { y } ) )
15 14 necomd 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( A \ { y } ) =/= A )
16 df-pss 
 |-  ( ( A \ { y } ) C. A <-> ( ( A \ { y } ) C_ A /\ ( A \ { y } ) =/= A ) )
17 10 15 16 sylanbrc 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( A \ { y } ) C. A )
18 php3 
 |-  ( ( A e. Fin /\ ( A \ { y } ) C. A ) -> ( A \ { y } ) ~< A )
19 9 17 18 syl2anc 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( A \ { y } ) ~< A )
20 6 ad2antrr 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> A ~~ B )
21 sdomentr 
 |-  ( ( ( A \ { y } ) ~< A /\ A ~~ B ) -> ( A \ { y } ) ~< B )
22 19 20 21 syl2anc 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( A \ { y } ) ~< B )
23 4 22 nsyl3 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> -. B ~<_ ( A \ { y } ) )
24 8 adantr 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> A e. Fin )
25 difss 
 |-  ( A \ { y } ) C_ A
26 ssfi 
 |-  ( ( A e. Fin /\ ( A \ { y } ) C_ A ) -> ( A \ { y } ) e. Fin )
27 24 25 26 sylancl 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> ( A \ { y } ) e. Fin )
28 3 adantr 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> F : A --> B )
29 fssres 
 |-  ( ( F : A --> B /\ ( A \ { y } ) C_ A ) -> ( F |` ( A \ { y } ) ) : ( A \ { y } ) --> B )
30 28 25 29 sylancl 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> ( F |` ( A \ { y } ) ) : ( A \ { y } ) --> B )
31 1 adantr 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> F : A -onto-> B )
32 foelrn 
 |-  ( ( F : A -onto-> B /\ z e. B ) -> E. u e. A z = ( F ` u ) )
33 31 32 sylan 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) /\ z e. B ) -> E. u e. A z = ( F ` u ) )
34 simprll 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> x e. A )
35 simprrr 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> x =/= y )
36 eldifsn 
 |-  ( x e. ( A \ { y } ) <-> ( x e. A /\ x =/= y ) )
37 34 35 36 sylanbrc 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> x e. ( A \ { y } ) )
38 simprrl 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> ( F ` x ) = ( F ` y ) )
39 38 eqcomd 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> ( F ` y ) = ( F ` x ) )
40 fveq2 
 |-  ( w = x -> ( F ` w ) = ( F ` x ) )
41 40 rspceeqv 
 |-  ( ( x e. ( A \ { y } ) /\ ( F ` y ) = ( F ` x ) ) -> E. w e. ( A \ { y } ) ( F ` y ) = ( F ` w ) )
42 37 39 41 syl2anc 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> E. w e. ( A \ { y } ) ( F ` y ) = ( F ` w ) )
43 fveqeq2 
 |-  ( u = y -> ( ( F ` u ) = ( F ` w ) <-> ( F ` y ) = ( F ` w ) ) )
44 43 rexbidv 
 |-  ( u = y -> ( E. w e. ( A \ { y } ) ( F ` u ) = ( F ` w ) <-> E. w e. ( A \ { y } ) ( F ` y ) = ( F ` w ) ) )
45 42 44 syl5ibrcom 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> ( u = y -> E. w e. ( A \ { y } ) ( F ` u ) = ( F ` w ) ) )
46 45 adantr 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) /\ u e. A ) -> ( u = y -> E. w e. ( A \ { y } ) ( F ` u ) = ( F ` w ) ) )
47 46 imp 
 |-  ( ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) /\ u e. A ) /\ u = y ) -> E. w e. ( A \ { y } ) ( F ` u ) = ( F ` w ) )
48 eldifsn 
 |-  ( u e. ( A \ { y } ) <-> ( u e. A /\ u =/= y ) )
49 eqid 
 |-  ( F ` u ) = ( F ` u )
50 fveq2 
 |-  ( w = u -> ( F ` w ) = ( F ` u ) )
51 50 rspceeqv 
 |-  ( ( u e. ( A \ { y } ) /\ ( F ` u ) = ( F ` u ) ) -> E. w e. ( A \ { y } ) ( F ` u ) = ( F ` w ) )
52 49 51 mpan2 
 |-  ( u e. ( A \ { y } ) -> E. w e. ( A \ { y } ) ( F ` u ) = ( F ` w ) )
53 48 52 sylbir 
 |-  ( ( u e. A /\ u =/= y ) -> E. w e. ( A \ { y } ) ( F ` u ) = ( F ` w ) )
54 53 adantll 
 |-  ( ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) /\ u e. A ) /\ u =/= y ) -> E. w e. ( A \ { y } ) ( F ` u ) = ( F ` w ) )
55 47 54 pm2.61dane 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) /\ u e. A ) -> E. w e. ( A \ { y } ) ( F ` u ) = ( F ` w ) )
56 fvres 
 |-  ( w e. ( A \ { y } ) -> ( ( F |` ( A \ { y } ) ) ` w ) = ( F ` w ) )
57 56 eqeq2d 
 |-  ( w e. ( A \ { y } ) -> ( z = ( ( F |` ( A \ { y } ) ) ` w ) <-> z = ( F ` w ) ) )
58 57 rexbiia 
 |-  ( E. w e. ( A \ { y } ) z = ( ( F |` ( A \ { y } ) ) ` w ) <-> E. w e. ( A \ { y } ) z = ( F ` w ) )
59 eqeq1 
 |-  ( z = ( F ` u ) -> ( z = ( F ` w ) <-> ( F ` u ) = ( F ` w ) ) )
60 59 rexbidv 
 |-  ( z = ( F ` u ) -> ( E. w e. ( A \ { y } ) z = ( F ` w ) <-> E. w e. ( A \ { y } ) ( F ` u ) = ( F ` w ) ) )
61 58 60 bitrid 
 |-  ( z = ( F ` u ) -> ( E. w e. ( A \ { y } ) z = ( ( F |` ( A \ { y } ) ) ` w ) <-> E. w e. ( A \ { y } ) ( F ` u ) = ( F ` w ) ) )
62 55 61 syl5ibrcom 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) /\ u e. A ) -> ( z = ( F ` u ) -> E. w e. ( A \ { y } ) z = ( ( F |` ( A \ { y } ) ) ` w ) ) )
63 62 rexlimdva 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> ( E. u e. A z = ( F ` u ) -> E. w e. ( A \ { y } ) z = ( ( F |` ( A \ { y } ) ) ` w ) ) )
64 63 imp 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) /\ E. u e. A z = ( F ` u ) ) -> E. w e. ( A \ { y } ) z = ( ( F |` ( A \ { y } ) ) ` w ) )
65 33 64 syldan 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) /\ z e. B ) -> E. w e. ( A \ { y } ) z = ( ( F |` ( A \ { y } ) ) ` w ) )
66 65 ralrimiva 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> A. z e. B E. w e. ( A \ { y } ) z = ( ( F |` ( A \ { y } ) ) ` w ) )
67 dffo3 
 |-  ( ( F |` ( A \ { y } ) ) : ( A \ { y } ) -onto-> B <-> ( ( F |` ( A \ { y } ) ) : ( A \ { y } ) --> B /\ A. z e. B E. w e. ( A \ { y } ) z = ( ( F |` ( A \ { y } ) ) ` w ) ) )
68 30 66 67 sylanbrc 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> ( F |` ( A \ { y } ) ) : ( A \ { y } ) -onto-> B )
69 fodomfi 
 |-  ( ( ( A \ { y } ) e. Fin /\ ( F |` ( A \ { y } ) ) : ( A \ { y } ) -onto-> B ) -> B ~<_ ( A \ { y } ) )
70 27 68 69 syl2anc 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) -> B ~<_ ( A \ { y } ) )
71 70 anassrs 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) -> B ~<_ ( A \ { y } ) )
72 71 expr 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( x =/= y -> B ~<_ ( A \ { y } ) ) )
73 72 necon1bd 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( -. B ~<_ ( A \ { y } ) -> x = y ) )
74 23 73 mpd 
 |-  ( ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> x = y )
75 74 ex 
 |-  ( ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) /\ ( x e. A /\ y e. A ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
76 75 ralrimivva 
 |-  ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) -> A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) )
77 dff13 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
78 3 76 77 sylanbrc 
 |-  ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) -> F : A -1-1-> B )
79 df-f1o 
 |-  ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
80 78 1 79 sylanbrc 
 |-  ( ( F : A -onto-> B /\ A ~~ B /\ B e. Fin ) -> F : A -1-1-onto-> B )