Metamath Proof Explorer

Theorem ackbij1lem5

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 19-Nov-2014) (Proof shortened by AV, 18-Jul-2022)

Ref Expression
Assertion ackbij1lem5 
|- ( A e. _om -> ( card ` ~P suc A ) = ( ( card ` ~P A ) +o ( card ` ~P A ) ) )

Proof

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