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