Step |
Hyp |
Ref |
Expression |
1 |
|
relsdom |
|- Rel ~< |
2 |
1
|
brrelex2i |
|- ( (/) ~< B -> B e. _V ) |
3 |
|
0sdomg |
|- ( B e. _V -> ( (/) ~< B <-> B =/= (/) ) ) |
4 |
|
n0 |
|- ( B =/= (/) <-> E. z z e. B ) |
5 |
3 4
|
bitrdi |
|- ( B e. _V -> ( (/) ~< B <-> E. z z e. B ) ) |
6 |
2 5
|
syl |
|- ( (/) ~< B -> ( (/) ~< B <-> E. z z e. B ) ) |
7 |
6
|
ibi |
|- ( (/) ~< B -> E. z z e. B ) |
8 |
|
domfi |
|- ( ( A e. Fin /\ B ~<_ A ) -> B e. Fin ) |
9 |
|
simpl |
|- ( ( A e. Fin /\ B ~<_ A ) -> A e. Fin ) |
10 |
|
brdomi |
|- ( B ~<_ A -> E. g g : B -1-1-> A ) |
11 |
|
f1fn |
|- ( g : B -1-1-> A -> g Fn B ) |
12 |
|
fnfi |
|- ( ( g Fn B /\ B e. Fin ) -> g e. Fin ) |
13 |
11 12
|
sylan |
|- ( ( g : B -1-1-> A /\ B e. Fin ) -> g e. Fin ) |
14 |
13
|
ex |
|- ( g : B -1-1-> A -> ( B e. Fin -> g e. Fin ) ) |
15 |
|
cnvfi |
|- ( g e. Fin -> `' g e. Fin ) |
16 |
|
diffi |
|- ( A e. Fin -> ( A \ ran g ) e. Fin ) |
17 |
|
snfi |
|- { z } e. Fin |
18 |
|
xpfi |
|- ( ( ( A \ ran g ) e. Fin /\ { z } e. Fin ) -> ( ( A \ ran g ) X. { z } ) e. Fin ) |
19 |
16 17 18
|
sylancl |
|- ( A e. Fin -> ( ( A \ ran g ) X. { z } ) e. Fin ) |
20 |
|
unfi |
|- ( ( `' g e. Fin /\ ( ( A \ ran g ) X. { z } ) e. Fin ) -> ( `' g u. ( ( A \ ran g ) X. { z } ) ) e. Fin ) |
21 |
15 19 20
|
syl2an |
|- ( ( g e. Fin /\ A e. Fin ) -> ( `' g u. ( ( A \ ran g ) X. { z } ) ) e. Fin ) |
22 |
|
df-f1 |
|- ( g : B -1-1-> A <-> ( g : B --> A /\ Fun `' g ) ) |
23 |
22
|
simprbi |
|- ( g : B -1-1-> A -> Fun `' g ) |
24 |
|
vex |
|- z e. _V |
25 |
24
|
fconst |
|- ( ( A \ ran g ) X. { z } ) : ( A \ ran g ) --> { z } |
26 |
|
ffun |
|- ( ( ( A \ ran g ) X. { z } ) : ( A \ ran g ) --> { z } -> Fun ( ( A \ ran g ) X. { z } ) ) |
27 |
25 26
|
ax-mp |
|- Fun ( ( A \ ran g ) X. { z } ) |
28 |
23 27
|
jctir |
|- ( g : B -1-1-> A -> ( Fun `' g /\ Fun ( ( A \ ran g ) X. { z } ) ) ) |
29 |
|
df-rn |
|- ran g = dom `' g |
30 |
29
|
eqcomi |
|- dom `' g = ran g |
31 |
24
|
snnz |
|- { z } =/= (/) |
32 |
|
dmxp |
|- ( { z } =/= (/) -> dom ( ( A \ ran g ) X. { z } ) = ( A \ ran g ) ) |
33 |
31 32
|
ax-mp |
|- dom ( ( A \ ran g ) X. { z } ) = ( A \ ran g ) |
34 |
30 33
|
ineq12i |
|- ( dom `' g i^i dom ( ( A \ ran g ) X. { z } ) ) = ( ran g i^i ( A \ ran g ) ) |
35 |
|
disjdif |
|- ( ran g i^i ( A \ ran g ) ) = (/) |
36 |
34 35
|
eqtri |
|- ( dom `' g i^i dom ( ( A \ ran g ) X. { z } ) ) = (/) |
37 |
|
funun |
|- ( ( ( Fun `' g /\ Fun ( ( A \ ran g ) X. { z } ) ) /\ ( dom `' g i^i dom ( ( A \ ran g ) X. { z } ) ) = (/) ) -> Fun ( `' g u. ( ( A \ ran g ) X. { z } ) ) ) |
38 |
28 36 37
|
sylancl |
|- ( g : B -1-1-> A -> Fun ( `' g u. ( ( A \ ran g ) X. { z } ) ) ) |
39 |
38
|
adantl |
|- ( ( z e. B /\ g : B -1-1-> A ) -> Fun ( `' g u. ( ( A \ ran g ) X. { z } ) ) ) |
40 |
|
dmun |
|- dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = ( dom `' g u. dom ( ( A \ ran g ) X. { z } ) ) |
41 |
29
|
uneq1i |
|- ( ran g u. dom ( ( A \ ran g ) X. { z } ) ) = ( dom `' g u. dom ( ( A \ ran g ) X. { z } ) ) |
42 |
33
|
uneq2i |
|- ( ran g u. dom ( ( A \ ran g ) X. { z } ) ) = ( ran g u. ( A \ ran g ) ) |
43 |
40 41 42
|
3eqtr2i |
|- dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = ( ran g u. ( A \ ran g ) ) |
44 |
|
f1f |
|- ( g : B -1-1-> A -> g : B --> A ) |
45 |
44
|
frnd |
|- ( g : B -1-1-> A -> ran g C_ A ) |
46 |
|
undif |
|- ( ran g C_ A <-> ( ran g u. ( A \ ran g ) ) = A ) |
47 |
45 46
|
sylib |
|- ( g : B -1-1-> A -> ( ran g u. ( A \ ran g ) ) = A ) |
48 |
43 47
|
eqtrid |
|- ( g : B -1-1-> A -> dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = A ) |
49 |
48
|
adantl |
|- ( ( z e. B /\ g : B -1-1-> A ) -> dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = A ) |
50 |
|
df-fn |
|- ( ( `' g u. ( ( A \ ran g ) X. { z } ) ) Fn A <-> ( Fun ( `' g u. ( ( A \ ran g ) X. { z } ) ) /\ dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = A ) ) |
51 |
39 49 50
|
sylanbrc |
|- ( ( z e. B /\ g : B -1-1-> A ) -> ( `' g u. ( ( A \ ran g ) X. { z } ) ) Fn A ) |
52 |
|
rnun |
|- ran ( `' g u. ( ( A \ ran g ) X. { z } ) ) = ( ran `' g u. ran ( ( A \ ran g ) X. { z } ) ) |
53 |
|
dfdm4 |
|- dom g = ran `' g |
54 |
|
f1dm |
|- ( g : B -1-1-> A -> dom g = B ) |
55 |
53 54
|
eqtr3id |
|- ( g : B -1-1-> A -> ran `' g = B ) |
56 |
55
|
uneq1d |
|- ( g : B -1-1-> A -> ( ran `' g u. ran ( ( A \ ran g ) X. { z } ) ) = ( B u. ran ( ( A \ ran g ) X. { z } ) ) ) |
57 |
|
xpeq1 |
|- ( ( A \ ran g ) = (/) -> ( ( A \ ran g ) X. { z } ) = ( (/) X. { z } ) ) |
58 |
|
0xp |
|- ( (/) X. { z } ) = (/) |
59 |
57 58
|
eqtrdi |
|- ( ( A \ ran g ) = (/) -> ( ( A \ ran g ) X. { z } ) = (/) ) |
60 |
59
|
rneqd |
|- ( ( A \ ran g ) = (/) -> ran ( ( A \ ran g ) X. { z } ) = ran (/) ) |
61 |
|
rn0 |
|- ran (/) = (/) |
62 |
60 61
|
eqtrdi |
|- ( ( A \ ran g ) = (/) -> ran ( ( A \ ran g ) X. { z } ) = (/) ) |
63 |
|
0ss |
|- (/) C_ B |
64 |
62 63
|
eqsstrdi |
|- ( ( A \ ran g ) = (/) -> ran ( ( A \ ran g ) X. { z } ) C_ B ) |
65 |
64
|
a1d |
|- ( ( A \ ran g ) = (/) -> ( z e. B -> ran ( ( A \ ran g ) X. { z } ) C_ B ) ) |
66 |
|
rnxp |
|- ( ( A \ ran g ) =/= (/) -> ran ( ( A \ ran g ) X. { z } ) = { z } ) |
67 |
66
|
adantr |
|- ( ( ( A \ ran g ) =/= (/) /\ z e. B ) -> ran ( ( A \ ran g ) X. { z } ) = { z } ) |
68 |
|
snssi |
|- ( z e. B -> { z } C_ B ) |
69 |
68
|
adantl |
|- ( ( ( A \ ran g ) =/= (/) /\ z e. B ) -> { z } C_ B ) |
70 |
67 69
|
eqsstrd |
|- ( ( ( A \ ran g ) =/= (/) /\ z e. B ) -> ran ( ( A \ ran g ) X. { z } ) C_ B ) |
71 |
70
|
ex |
|- ( ( A \ ran g ) =/= (/) -> ( z e. B -> ran ( ( A \ ran g ) X. { z } ) C_ B ) ) |
72 |
65 71
|
pm2.61ine |
|- ( z e. B -> ran ( ( A \ ran g ) X. { z } ) C_ B ) |
73 |
|
ssequn2 |
|- ( ran ( ( A \ ran g ) X. { z } ) C_ B <-> ( B u. ran ( ( A \ ran g ) X. { z } ) ) = B ) |
74 |
72 73
|
sylib |
|- ( z e. B -> ( B u. ran ( ( A \ ran g ) X. { z } ) ) = B ) |
75 |
56 74
|
sylan9eqr |
|- ( ( z e. B /\ g : B -1-1-> A ) -> ( ran `' g u. ran ( ( A \ ran g ) X. { z } ) ) = B ) |
76 |
52 75
|
eqtrid |
|- ( ( z e. B /\ g : B -1-1-> A ) -> ran ( `' g u. ( ( A \ ran g ) X. { z } ) ) = B ) |
77 |
|
df-fo |
|- ( ( `' g u. ( ( A \ ran g ) X. { z } ) ) : A -onto-> B <-> ( ( `' g u. ( ( A \ ran g ) X. { z } ) ) Fn A /\ ran ( `' g u. ( ( A \ ran g ) X. { z } ) ) = B ) ) |
78 |
51 76 77
|
sylanbrc |
|- ( ( z e. B /\ g : B -1-1-> A ) -> ( `' g u. ( ( A \ ran g ) X. { z } ) ) : A -onto-> B ) |
79 |
|
foeq1 |
|- ( f = ( `' g u. ( ( A \ ran g ) X. { z } ) ) -> ( f : A -onto-> B <-> ( `' g u. ( ( A \ ran g ) X. { z } ) ) : A -onto-> B ) ) |
80 |
79
|
spcegv |
|- ( ( `' g u. ( ( A \ ran g ) X. { z } ) ) e. Fin -> ( ( `' g u. ( ( A \ ran g ) X. { z } ) ) : A -onto-> B -> E. f f : A -onto-> B ) ) |
81 |
21 78 80
|
syl2im |
|- ( ( g e. Fin /\ A e. Fin ) -> ( ( z e. B /\ g : B -1-1-> A ) -> E. f f : A -onto-> B ) ) |
82 |
81
|
expcomd |
|- ( ( g e. Fin /\ A e. Fin ) -> ( g : B -1-1-> A -> ( z e. B -> E. f f : A -onto-> B ) ) ) |
83 |
82
|
com12 |
|- ( g : B -1-1-> A -> ( ( g e. Fin /\ A e. Fin ) -> ( z e. B -> E. f f : A -onto-> B ) ) ) |
84 |
14 83
|
syland |
|- ( g : B -1-1-> A -> ( ( B e. Fin /\ A e. Fin ) -> ( z e. B -> E. f f : A -onto-> B ) ) ) |
85 |
84
|
exlimiv |
|- ( E. g g : B -1-1-> A -> ( ( B e. Fin /\ A e. Fin ) -> ( z e. B -> E. f f : A -onto-> B ) ) ) |
86 |
10 85
|
syl |
|- ( B ~<_ A -> ( ( B e. Fin /\ A e. Fin ) -> ( z e. B -> E. f f : A -onto-> B ) ) ) |
87 |
86
|
adantl |
|- ( ( A e. Fin /\ B ~<_ A ) -> ( ( B e. Fin /\ A e. Fin ) -> ( z e. B -> E. f f : A -onto-> B ) ) ) |
88 |
8 9 87
|
mp2and |
|- ( ( A e. Fin /\ B ~<_ A ) -> ( z e. B -> E. f f : A -onto-> B ) ) |
89 |
88
|
exlimdv |
|- ( ( A e. Fin /\ B ~<_ A ) -> ( E. z z e. B -> E. f f : A -onto-> B ) ) |
90 |
7 89
|
syl5 |
|- ( ( A e. Fin /\ B ~<_ A ) -> ( (/) ~< B -> E. f f : A -onto-> B ) ) |
91 |
90
|
3impia |
|- ( ( A e. Fin /\ B ~<_ A /\ (/) ~< B ) -> E. f f : A -onto-> B ) |
92 |
91
|
3com23 |
|- ( ( A e. Fin /\ (/) ~< B /\ B ~<_ A ) -> E. f f : A -onto-> B ) |