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 syl5bb
 |-  ( 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 )