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