Step |
Hyp |
Ref |
Expression |
1 |
|
ackbij.f |
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) ) |
2 |
1
|
ackbij1lem17 |
|- F : ( ~P _om i^i Fin ) -1-1-> _om |
3 |
|
ackbij2lem1 |
|- ( A e. _om -> ~P A C_ ( ~P _om i^i Fin ) ) |
4 |
|
pwexg |
|- ( A e. _om -> ~P A e. _V ) |
5 |
|
f1imaeng |
|- ( ( F : ( ~P _om i^i Fin ) -1-1-> _om /\ ~P A C_ ( ~P _om i^i Fin ) /\ ~P A e. _V ) -> ( F " ~P A ) ~~ ~P A ) |
6 |
2 3 4 5
|
mp3an2i |
|- ( A e. _om -> ( F " ~P A ) ~~ ~P A ) |
7 |
|
nnfi |
|- ( A e. _om -> A e. Fin ) |
8 |
|
pwfi |
|- ( A e. Fin <-> ~P A e. Fin ) |
9 |
7 8
|
sylib |
|- ( A e. _om -> ~P A e. Fin ) |
10 |
|
ficardid |
|- ( ~P A e. Fin -> ( card ` ~P A ) ~~ ~P A ) |
11 |
|
ensym |
|- ( ( card ` ~P A ) ~~ ~P A -> ~P A ~~ ( card ` ~P A ) ) |
12 |
9 10 11
|
3syl |
|- ( A e. _om -> ~P A ~~ ( card ` ~P A ) ) |
13 |
|
entr |
|- ( ( ( F " ~P A ) ~~ ~P A /\ ~P A ~~ ( card ` ~P A ) ) -> ( F " ~P A ) ~~ ( card ` ~P A ) ) |
14 |
6 12 13
|
syl2anc |
|- ( A e. _om -> ( F " ~P A ) ~~ ( card ` ~P A ) ) |
15 |
|
onfin2 |
|- _om = ( On i^i Fin ) |
16 |
|
inss2 |
|- ( On i^i Fin ) C_ Fin |
17 |
15 16
|
eqsstri |
|- _om C_ Fin |
18 |
|
ficardom |
|- ( ~P A e. Fin -> ( card ` ~P A ) e. _om ) |
19 |
9 18
|
syl |
|- ( A e. _om -> ( card ` ~P A ) e. _om ) |
20 |
17 19
|
sselid |
|- ( A e. _om -> ( card ` ~P A ) e. Fin ) |
21 |
|
php3 |
|- ( ( ( card ` ~P A ) e. Fin /\ ( F " ~P A ) C. ( card ` ~P A ) ) -> ( F " ~P A ) ~< ( card ` ~P A ) ) |
22 |
21
|
ex |
|- ( ( card ` ~P A ) e. Fin -> ( ( F " ~P A ) C. ( card ` ~P A ) -> ( F " ~P A ) ~< ( card ` ~P A ) ) ) |
23 |
20 22
|
syl |
|- ( A e. _om -> ( ( F " ~P A ) C. ( card ` ~P A ) -> ( F " ~P A ) ~< ( card ` ~P A ) ) ) |
24 |
|
sdomnen |
|- ( ( F " ~P A ) ~< ( card ` ~P A ) -> -. ( F " ~P A ) ~~ ( card ` ~P A ) ) |
25 |
23 24
|
syl6 |
|- ( A e. _om -> ( ( F " ~P A ) C. ( card ` ~P A ) -> -. ( F " ~P A ) ~~ ( card ` ~P A ) ) ) |
26 |
14 25
|
mt2d |
|- ( A e. _om -> -. ( F " ~P A ) C. ( card ` ~P A ) ) |
27 |
|
fvex |
|- ( F ` a ) e. _V |
28 |
|
ackbij1lem3 |
|- ( A e. _om -> A e. ( ~P _om i^i Fin ) ) |
29 |
|
elpwi |
|- ( a e. ~P A -> a C_ A ) |
30 |
1
|
ackbij1lem12 |
|- ( ( A e. ( ~P _om i^i Fin ) /\ a C_ A ) -> ( F ` a ) C_ ( F ` A ) ) |
31 |
28 29 30
|
syl2an |
|- ( ( A e. _om /\ a e. ~P A ) -> ( F ` a ) C_ ( F ` A ) ) |
32 |
1
|
ackbij1lem10 |
|- F : ( ~P _om i^i Fin ) --> _om |
33 |
|
peano1 |
|- (/) e. _om |
34 |
32 33
|
f0cli |
|- ( F ` a ) e. _om |
35 |
|
nnord |
|- ( ( F ` a ) e. _om -> Ord ( F ` a ) ) |
36 |
34 35
|
ax-mp |
|- Ord ( F ` a ) |
37 |
32 33
|
f0cli |
|- ( F ` A ) e. _om |
38 |
|
nnord |
|- ( ( F ` A ) e. _om -> Ord ( F ` A ) ) |
39 |
37 38
|
ax-mp |
|- Ord ( F ` A ) |
40 |
|
ordsucsssuc |
|- ( ( Ord ( F ` a ) /\ Ord ( F ` A ) ) -> ( ( F ` a ) C_ ( F ` A ) <-> suc ( F ` a ) C_ suc ( F ` A ) ) ) |
41 |
36 39 40
|
mp2an |
|- ( ( F ` a ) C_ ( F ` A ) <-> suc ( F ` a ) C_ suc ( F ` A ) ) |
42 |
31 41
|
sylib |
|- ( ( A e. _om /\ a e. ~P A ) -> suc ( F ` a ) C_ suc ( F ` A ) ) |
43 |
1
|
ackbij1lem14 |
|- ( A e. _om -> ( F ` { A } ) = suc ( F ` A ) ) |
44 |
1
|
ackbij1lem8 |
|- ( A e. _om -> ( F ` { A } ) = ( card ` ~P A ) ) |
45 |
43 44
|
eqtr3d |
|- ( A e. _om -> suc ( F ` A ) = ( card ` ~P A ) ) |
46 |
45
|
adantr |
|- ( ( A e. _om /\ a e. ~P A ) -> suc ( F ` A ) = ( card ` ~P A ) ) |
47 |
42 46
|
sseqtrd |
|- ( ( A e. _om /\ a e. ~P A ) -> suc ( F ` a ) C_ ( card ` ~P A ) ) |
48 |
|
sucssel |
|- ( ( F ` a ) e. _V -> ( suc ( F ` a ) C_ ( card ` ~P A ) -> ( F ` a ) e. ( card ` ~P A ) ) ) |
49 |
27 47 48
|
mpsyl |
|- ( ( A e. _om /\ a e. ~P A ) -> ( F ` a ) e. ( card ` ~P A ) ) |
50 |
49
|
ralrimiva |
|- ( A e. _om -> A. a e. ~P A ( F ` a ) e. ( card ` ~P A ) ) |
51 |
|
f1fun |
|- ( F : ( ~P _om i^i Fin ) -1-1-> _om -> Fun F ) |
52 |
2 51
|
ax-mp |
|- Fun F |
53 |
|
f1dm |
|- ( F : ( ~P _om i^i Fin ) -1-1-> _om -> dom F = ( ~P _om i^i Fin ) ) |
54 |
2 53
|
ax-mp |
|- dom F = ( ~P _om i^i Fin ) |
55 |
3 54
|
sseqtrrdi |
|- ( A e. _om -> ~P A C_ dom F ) |
56 |
|
funimass4 |
|- ( ( Fun F /\ ~P A C_ dom F ) -> ( ( F " ~P A ) C_ ( card ` ~P A ) <-> A. a e. ~P A ( F ` a ) e. ( card ` ~P A ) ) ) |
57 |
52 55 56
|
sylancr |
|- ( A e. _om -> ( ( F " ~P A ) C_ ( card ` ~P A ) <-> A. a e. ~P A ( F ` a ) e. ( card ` ~P A ) ) ) |
58 |
50 57
|
mpbird |
|- ( A e. _om -> ( F " ~P A ) C_ ( card ` ~P A ) ) |
59 |
|
sspss |
|- ( ( F " ~P A ) C_ ( card ` ~P A ) <-> ( ( F " ~P A ) C. ( card ` ~P A ) \/ ( F " ~P A ) = ( card ` ~P A ) ) ) |
60 |
58 59
|
sylib |
|- ( A e. _om -> ( ( F " ~P A ) C. ( card ` ~P A ) \/ ( F " ~P A ) = ( card ` ~P A ) ) ) |
61 |
|
orel1 |
|- ( -. ( F " ~P A ) C. ( card ` ~P A ) -> ( ( ( F " ~P A ) C. ( card ` ~P A ) \/ ( F " ~P A ) = ( card ` ~P A ) ) -> ( F " ~P A ) = ( card ` ~P A ) ) ) |
62 |
26 60 61
|
sylc |
|- ( A e. _om -> ( F " ~P A ) = ( card ` ~P A ) ) |