Step |
Hyp |
Ref |
Expression |
1 |
|
peano2 |
|- ( A e. _om -> suc A e. _om ) |
2 |
|
pw2eng |
|- ( suc A e. _om -> ~P suc A ~~ ( 2o ^m suc A ) ) |
3 |
1 2
|
syl |
|- ( A e. _om -> ~P suc A ~~ ( 2o ^m suc A ) ) |
4 |
|
df-suc |
|- suc A = ( A u. { A } ) |
5 |
4
|
oveq2i |
|- ( 2o ^m suc A ) = ( 2o ^m ( A u. { A } ) ) |
6 |
|
elex |
|- ( A e. _om -> A e. _V ) |
7 |
|
snex |
|- { A } e. _V |
8 |
7
|
a1i |
|- ( A e. _om -> { A } e. _V ) |
9 |
|
2onn |
|- 2o e. _om |
10 |
9
|
elexi |
|- 2o e. _V |
11 |
10
|
a1i |
|- ( A e. _om -> 2o e. _V ) |
12 |
|
nnord |
|- ( A e. _om -> Ord A ) |
13 |
|
orddisj |
|- ( Ord A -> ( A i^i { A } ) = (/) ) |
14 |
12 13
|
syl |
|- ( A e. _om -> ( A i^i { A } ) = (/) ) |
15 |
|
mapunen |
|- ( ( ( A e. _V /\ { A } e. _V /\ 2o e. _V ) /\ ( A i^i { A } ) = (/) ) -> ( 2o ^m ( A u. { A } ) ) ~~ ( ( 2o ^m A ) X. ( 2o ^m { A } ) ) ) |
16 |
6 8 11 14 15
|
syl31anc |
|- ( A e. _om -> ( 2o ^m ( A u. { A } ) ) ~~ ( ( 2o ^m A ) X. ( 2o ^m { A } ) ) ) |
17 |
|
ovex |
|- ( 2o ^m A ) e. _V |
18 |
17
|
enref |
|- ( 2o ^m A ) ~~ ( 2o ^m A ) |
19 |
|
2on |
|- 2o e. On |
20 |
19
|
a1i |
|- ( A e. _om -> 2o e. On ) |
21 |
|
id |
|- ( A e. _om -> A e. _om ) |
22 |
20 21
|
mapsnend |
|- ( A e. _om -> ( 2o ^m { A } ) ~~ 2o ) |
23 |
|
xpen |
|- ( ( ( 2o ^m A ) ~~ ( 2o ^m A ) /\ ( 2o ^m { A } ) ~~ 2o ) -> ( ( 2o ^m A ) X. ( 2o ^m { A } ) ) ~~ ( ( 2o ^m A ) X. 2o ) ) |
24 |
18 22 23
|
sylancr |
|- ( A e. _om -> ( ( 2o ^m A ) X. ( 2o ^m { A } ) ) ~~ ( ( 2o ^m A ) X. 2o ) ) |
25 |
|
entr |
|- ( ( ( 2o ^m ( A u. { A } ) ) ~~ ( ( 2o ^m A ) X. ( 2o ^m { A } ) ) /\ ( ( 2o ^m A ) X. ( 2o ^m { A } ) ) ~~ ( ( 2o ^m A ) X. 2o ) ) -> ( 2o ^m ( A u. { A } ) ) ~~ ( ( 2o ^m A ) X. 2o ) ) |
26 |
16 24 25
|
syl2anc |
|- ( A e. _om -> ( 2o ^m ( A u. { A } ) ) ~~ ( ( 2o ^m A ) X. 2o ) ) |
27 |
5 26
|
eqbrtrid |
|- ( A e. _om -> ( 2o ^m suc A ) ~~ ( ( 2o ^m A ) X. 2o ) ) |
28 |
17 10
|
xpcomen |
|- ( ( 2o ^m A ) X. 2o ) ~~ ( 2o X. ( 2o ^m A ) ) |
29 |
|
entr |
|- ( ( ( 2o ^m suc A ) ~~ ( ( 2o ^m A ) X. 2o ) /\ ( ( 2o ^m A ) X. 2o ) ~~ ( 2o X. ( 2o ^m A ) ) ) -> ( 2o ^m suc A ) ~~ ( 2o X. ( 2o ^m A ) ) ) |
30 |
27 28 29
|
sylancl |
|- ( A e. _om -> ( 2o ^m suc A ) ~~ ( 2o X. ( 2o ^m A ) ) ) |
31 |
10
|
enref |
|- 2o ~~ 2o |
32 |
|
pw2eng |
|- ( A e. _om -> ~P A ~~ ( 2o ^m A ) ) |
33 |
|
xpen |
|- ( ( 2o ~~ 2o /\ ~P A ~~ ( 2o ^m A ) ) -> ( 2o X. ~P A ) ~~ ( 2o X. ( 2o ^m A ) ) ) |
34 |
31 32 33
|
sylancr |
|- ( A e. _om -> ( 2o X. ~P A ) ~~ ( 2o X. ( 2o ^m A ) ) ) |
35 |
34
|
ensymd |
|- ( A e. _om -> ( 2o X. ( 2o ^m A ) ) ~~ ( 2o X. ~P A ) ) |
36 |
|
entr |
|- ( ( ( 2o ^m suc A ) ~~ ( 2o X. ( 2o ^m A ) ) /\ ( 2o X. ( 2o ^m A ) ) ~~ ( 2o X. ~P A ) ) -> ( 2o ^m suc A ) ~~ ( 2o X. ~P A ) ) |
37 |
30 35 36
|
syl2anc |
|- ( A e. _om -> ( 2o ^m suc A ) ~~ ( 2o X. ~P A ) ) |
38 |
|
entr |
|- ( ( ~P suc A ~~ ( 2o ^m suc A ) /\ ( 2o ^m suc A ) ~~ ( 2o X. ~P A ) ) -> ~P suc A ~~ ( 2o X. ~P A ) ) |
39 |
3 37 38
|
syl2anc |
|- ( A e. _om -> ~P suc A ~~ ( 2o X. ~P A ) ) |
40 |
|
xp2dju |
|- ( 2o X. ~P A ) = ( ~P A |_| ~P A ) |
41 |
39 40
|
breqtrdi |
|- ( A e. _om -> ~P suc A ~~ ( ~P A |_| ~P A ) ) |
42 |
|
nnfi |
|- ( A e. _om -> A e. Fin ) |
43 |
|
pwfi |
|- ( A e. Fin <-> ~P A e. Fin ) |
44 |
42 43
|
sylib |
|- ( A e. _om -> ~P A e. Fin ) |
45 |
|
ficardid |
|- ( ~P A e. Fin -> ( card ` ~P A ) ~~ ~P A ) |
46 |
44 45
|
syl |
|- ( A e. _om -> ( card ` ~P A ) ~~ ~P A ) |
47 |
|
djuen |
|- ( ( ( card ` ~P A ) ~~ ~P A /\ ( card ` ~P A ) ~~ ~P A ) -> ( ( card ` ~P A ) |_| ( card ` ~P A ) ) ~~ ( ~P A |_| ~P A ) ) |
48 |
46 46 47
|
syl2anc |
|- ( A e. _om -> ( ( card ` ~P A ) |_| ( card ` ~P A ) ) ~~ ( ~P A |_| ~P A ) ) |
49 |
48
|
ensymd |
|- ( A e. _om -> ( ~P A |_| ~P A ) ~~ ( ( card ` ~P A ) |_| ( card ` ~P A ) ) ) |
50 |
|
entr |
|- ( ( ~P suc A ~~ ( ~P A |_| ~P A ) /\ ( ~P A |_| ~P A ) ~~ ( ( card ` ~P A ) |_| ( card ` ~P A ) ) ) -> ~P suc A ~~ ( ( card ` ~P A ) |_| ( card ` ~P A ) ) ) |
51 |
41 49 50
|
syl2anc |
|- ( A e. _om -> ~P suc A ~~ ( ( card ` ~P A ) |_| ( card ` ~P A ) ) ) |
52 |
|
carden2b |
|- ( ~P suc A ~~ ( ( card ` ~P A ) |_| ( card ` ~P A ) ) -> ( card ` ~P suc A ) = ( card ` ( ( card ` ~P A ) |_| ( card ` ~P A ) ) ) ) |
53 |
51 52
|
syl |
|- ( A e. _om -> ( card ` ~P suc A ) = ( card ` ( ( card ` ~P A ) |_| ( card ` ~P A ) ) ) ) |
54 |
|
ficardom |
|- ( ~P A e. Fin -> ( card ` ~P A ) e. _om ) |
55 |
44 54
|
syl |
|- ( A e. _om -> ( card ` ~P A ) e. _om ) |
56 |
|
nnadju |
|- ( ( ( card ` ~P A ) e. _om /\ ( card ` ~P A ) e. _om ) -> ( card ` ( ( card ` ~P A ) |_| ( card ` ~P A ) ) ) = ( ( card ` ~P A ) +o ( card ` ~P A ) ) ) |
57 |
55 55 56
|
syl2anc |
|- ( A e. _om -> ( card ` ( ( card ` ~P A ) |_| ( card ` ~P A ) ) ) = ( ( card ` ~P A ) +o ( card ` ~P A ) ) ) |
58 |
53 57
|
eqtrd |
|- ( A e. _om -> ( card ` ~P suc A ) = ( ( card ` ~P A ) +o ( card ` ~P A ) ) ) |