Step |
Hyp |
Ref |
Expression |
1 |
|
brdom3.2 |
|- B e. _V |
2 |
|
reldom |
|- Rel ~<_ |
3 |
2
|
brrelex1i |
|- ( A ~<_ B -> A e. _V ) |
4 |
|
0sdomg |
|- ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) ) |
5 |
3 4
|
syl |
|- ( A ~<_ B -> ( (/) ~< A <-> A =/= (/) ) ) |
6 |
|
df-ne |
|- ( A =/= (/) <-> -. A = (/) ) |
7 |
5 6
|
bitrdi |
|- ( A ~<_ B -> ( (/) ~< A <-> -. A = (/) ) ) |
8 |
7
|
biimpar |
|- ( ( A ~<_ B /\ -. A = (/) ) -> (/) ~< A ) |
9 |
|
fodomr |
|- ( ( (/) ~< A /\ A ~<_ B ) -> E. f f : B -onto-> A ) |
10 |
9
|
ancoms |
|- ( ( A ~<_ B /\ (/) ~< A ) -> E. f f : B -onto-> A ) |
11 |
8 10
|
syldan |
|- ( ( A ~<_ B /\ -. A = (/) ) -> E. f f : B -onto-> A ) |
12 |
|
pm5.6 |
|- ( ( ( A ~<_ B /\ -. A = (/) ) -> E. f f : B -onto-> A ) <-> ( A ~<_ B -> ( A = (/) \/ E. f f : B -onto-> A ) ) ) |
13 |
11 12
|
mpbi |
|- ( A ~<_ B -> ( A = (/) \/ E. f f : B -onto-> A ) ) |
14 |
|
br0 |
|- -. x (/) y |
15 |
14
|
nex |
|- -. E. y x (/) y |
16 |
|
exmo |
|- ( E. y x (/) y \/ E* y x (/) y ) |
17 |
15 16
|
mtpor |
|- E* y x (/) y |
18 |
17
|
ax-gen |
|- A. x E* y x (/) y |
19 |
|
rzal |
|- ( A = (/) -> A. x e. A E. y e. B y (/) x ) |
20 |
|
0ex |
|- (/) e. _V |
21 |
|
breq |
|- ( f = (/) -> ( x f y <-> x (/) y ) ) |
22 |
21
|
mobidv |
|- ( f = (/) -> ( E* y x f y <-> E* y x (/) y ) ) |
23 |
22
|
albidv |
|- ( f = (/) -> ( A. x E* y x f y <-> A. x E* y x (/) y ) ) |
24 |
|
breq |
|- ( f = (/) -> ( y f x <-> y (/) x ) ) |
25 |
24
|
rexbidv |
|- ( f = (/) -> ( E. y e. B y f x <-> E. y e. B y (/) x ) ) |
26 |
25
|
ralbidv |
|- ( f = (/) -> ( A. x e. A E. y e. B y f x <-> A. x e. A E. y e. B y (/) x ) ) |
27 |
23 26
|
anbi12d |
|- ( f = (/) -> ( ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) <-> ( A. x E* y x (/) y /\ A. x e. A E. y e. B y (/) x ) ) ) |
28 |
20 27
|
spcev |
|- ( ( A. x E* y x (/) y /\ A. x e. A E. y e. B y (/) x ) -> E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) ) |
29 |
18 19 28
|
sylancr |
|- ( A = (/) -> E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) ) |
30 |
|
fofun |
|- ( f : B -onto-> A -> Fun f ) |
31 |
|
dffun6 |
|- ( Fun f <-> ( Rel f /\ A. x E* y x f y ) ) |
32 |
31
|
simprbi |
|- ( Fun f -> A. x E* y x f y ) |
33 |
30 32
|
syl |
|- ( f : B -onto-> A -> A. x E* y x f y ) |
34 |
|
dffo4 |
|- ( f : B -onto-> A <-> ( f : B --> A /\ A. x e. A E. y e. B y f x ) ) |
35 |
34
|
simprbi |
|- ( f : B -onto-> A -> A. x e. A E. y e. B y f x ) |
36 |
33 35
|
jca |
|- ( f : B -onto-> A -> ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) ) |
37 |
36
|
eximi |
|- ( E. f f : B -onto-> A -> E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) ) |
38 |
29 37
|
jaoi |
|- ( ( A = (/) \/ E. f f : B -onto-> A ) -> E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) ) |
39 |
13 38
|
syl |
|- ( A ~<_ B -> E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) ) |
40 |
|
inss1 |
|- ( f i^i ( B X. A ) ) C_ f |
41 |
40
|
ssbri |
|- ( x ( f i^i ( B X. A ) ) y -> x f y ) |
42 |
41
|
moimi |
|- ( E* y x f y -> E* y x ( f i^i ( B X. A ) ) y ) |
43 |
42
|
alimi |
|- ( A. x E* y x f y -> A. x E* y x ( f i^i ( B X. A ) ) y ) |
44 |
|
relinxp |
|- Rel ( f i^i ( B X. A ) ) |
45 |
|
dffun6 |
|- ( Fun ( f i^i ( B X. A ) ) <-> ( Rel ( f i^i ( B X. A ) ) /\ A. x E* y x ( f i^i ( B X. A ) ) y ) ) |
46 |
44 45
|
mpbiran |
|- ( Fun ( f i^i ( B X. A ) ) <-> A. x E* y x ( f i^i ( B X. A ) ) y ) |
47 |
43 46
|
sylibr |
|- ( A. x E* y x f y -> Fun ( f i^i ( B X. A ) ) ) |
48 |
47
|
funfnd |
|- ( A. x E* y x f y -> ( f i^i ( B X. A ) ) Fn dom ( f i^i ( B X. A ) ) ) |
49 |
|
rninxp |
|- ( ran ( f i^i ( B X. A ) ) = A <-> A. x e. A E. y e. B y f x ) |
50 |
49
|
biimpri |
|- ( A. x e. A E. y e. B y f x -> ran ( f i^i ( B X. A ) ) = A ) |
51 |
48 50
|
anim12i |
|- ( ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) -> ( ( f i^i ( B X. A ) ) Fn dom ( f i^i ( B X. A ) ) /\ ran ( f i^i ( B X. A ) ) = A ) ) |
52 |
|
df-fo |
|- ( ( f i^i ( B X. A ) ) : dom ( f i^i ( B X. A ) ) -onto-> A <-> ( ( f i^i ( B X. A ) ) Fn dom ( f i^i ( B X. A ) ) /\ ran ( f i^i ( B X. A ) ) = A ) ) |
53 |
51 52
|
sylibr |
|- ( ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) -> ( f i^i ( B X. A ) ) : dom ( f i^i ( B X. A ) ) -onto-> A ) |
54 |
|
vex |
|- f e. _V |
55 |
54
|
inex1 |
|- ( f i^i ( B X. A ) ) e. _V |
56 |
55
|
dmex |
|- dom ( f i^i ( B X. A ) ) e. _V |
57 |
56
|
fodom |
|- ( ( f i^i ( B X. A ) ) : dom ( f i^i ( B X. A ) ) -onto-> A -> A ~<_ dom ( f i^i ( B X. A ) ) ) |
58 |
|
inss2 |
|- ( f i^i ( B X. A ) ) C_ ( B X. A ) |
59 |
|
dmss |
|- ( ( f i^i ( B X. A ) ) C_ ( B X. A ) -> dom ( f i^i ( B X. A ) ) C_ dom ( B X. A ) ) |
60 |
58 59
|
ax-mp |
|- dom ( f i^i ( B X. A ) ) C_ dom ( B X. A ) |
61 |
|
dmxpss |
|- dom ( B X. A ) C_ B |
62 |
60 61
|
sstri |
|- dom ( f i^i ( B X. A ) ) C_ B |
63 |
|
ssdomg |
|- ( B e. _V -> ( dom ( f i^i ( B X. A ) ) C_ B -> dom ( f i^i ( B X. A ) ) ~<_ B ) ) |
64 |
1 62 63
|
mp2 |
|- dom ( f i^i ( B X. A ) ) ~<_ B |
65 |
|
domtr |
|- ( ( A ~<_ dom ( f i^i ( B X. A ) ) /\ dom ( f i^i ( B X. A ) ) ~<_ B ) -> A ~<_ B ) |
66 |
64 65
|
mpan2 |
|- ( A ~<_ dom ( f i^i ( B X. A ) ) -> A ~<_ B ) |
67 |
53 57 66
|
3syl |
|- ( ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) -> A ~<_ B ) |
68 |
67
|
exlimiv |
|- ( E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) -> A ~<_ B ) |
69 |
39 68
|
impbii |
|- ( A ~<_ B <-> E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) ) |