This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ω → ( card ‘ 𝒫 suc 𝐴 ) = ( ( card ‘ 𝒫 𝐴 ) +o ( card ‘ 𝒫 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 peano2 ⊢ ( 𝐴 ∈ ω → suc 𝐴 ∈ ω )
2 pw2eng ⊢ ( suc 𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ ( 2o ↑m suc 𝐴 ) )
3 1 2 syl ⊢ ( 𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ ( 2o ↑m suc 𝐴 ) )
4 df-suc ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
5 4 oveq2i ⊢ ( 2o ↑m suc 𝐴 ) = ( 2o ↑m ( 𝐴 ∪ { 𝐴 } ) )
6 elex ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ V )
7 snex ⊢ { 𝐴 } ∈ V
8 7 a1i ⊢ ( 𝐴 ∈ ω → { 𝐴 } ∈ V )
9 2onn ⊢ 2o ∈ ω
10 9 elexi ⊢ 2o ∈ V
11 10 a1i ⊢ ( 𝐴 ∈ ω → 2o ∈ V )
12 nnord ⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
13 orddisj ⊢ ( Ord 𝐴 → ( 𝐴 ∩ { 𝐴 } ) = ∅ )
14 12 13 syl ⊢ ( 𝐴 ∈ ω → ( 𝐴 ∩ { 𝐴 } ) = ∅ )
15 mapunen ⊢ ( ( ( 𝐴 ∈ V ∧ { 𝐴 } ∈ V ∧ 2o ∈ V ) ∧ ( 𝐴 ∩ { 𝐴 } ) = ∅ ) → ( 2o ↑m ( 𝐴 ∪ { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m { 𝐴 } ) ) )
16 6 8 11 14 15 syl31anc ⊢ ( 𝐴 ∈ ω → ( 2o ↑m ( 𝐴 ∪ { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m { 𝐴 } ) ) )
17 ovex ⊢ ( 2o ↑m 𝐴 ) ∈ V
18 17 enref ⊢ ( 2o ↑m 𝐴 ) ≈ ( 2o ↑m 𝐴 )
19 2on ⊢ 2o ∈ On
20 19 a1i ⊢ ( 𝐴 ∈ ω → 2o ∈ On )
21 id ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ ω )
22 20 21 mapsnend ⊢ ( 𝐴 ∈ ω → ( 2o ↑m { 𝐴 } ) ≈ 2o )
23 xpen ⊢ ( ( ( 2o ↑m 𝐴 ) ≈ ( 2o ↑m 𝐴 ) ∧ ( 2o ↑m { 𝐴 } ) ≈ 2o ) → ( ( 2o ↑m 𝐴 ) × ( 2o ↑m { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) )
24 18 22 23 sylancr ⊢ ( 𝐴 ∈ ω → ( ( 2o ↑m 𝐴 ) × ( 2o ↑m { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) )
25 entr ⊢ ( ( ( 2o ↑m ( 𝐴 ∪ { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m { 𝐴 } ) ) ∧ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) ) → ( 2o ↑m ( 𝐴 ∪ { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) )
26 16 24 25 syl2anc ⊢ ( 𝐴 ∈ ω → ( 2o ↑m ( 𝐴 ∪ { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) )
27 5 26 eqbrtrid ⊢ ( 𝐴 ∈ ω → ( 2o ↑m suc 𝐴 ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) )
28 17 10 xpcomen ⊢ ( ( 2o ↑m 𝐴 ) × 2o ) ≈ ( 2o × ( 2o ↑m 𝐴 ) )
29 entr ⊢ ( ( ( 2o ↑m suc 𝐴 ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) ∧ ( ( 2o ↑m 𝐴 ) × 2o ) ≈ ( 2o × ( 2o ↑m 𝐴 ) ) ) → ( 2o ↑m suc 𝐴 ) ≈ ( 2o × ( 2o ↑m 𝐴 ) ) )
30 27 28 29 sylancl ⊢ ( 𝐴 ∈ ω → ( 2o ↑m suc 𝐴 ) ≈ ( 2o × ( 2o ↑m 𝐴 ) ) )
31 10 enref ⊢ 2o ≈ 2o
32 pw2eng ⊢ ( 𝐴 ∈ ω → 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) )
33 xpen ⊢ ( ( 2o ≈ 2o ∧ 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) ) → ( 2o × 𝒫 𝐴 ) ≈ ( 2o × ( 2o ↑m 𝐴 ) ) )
34 31 32 33 sylancr ⊢ ( 𝐴 ∈ ω → ( 2o × 𝒫 𝐴 ) ≈ ( 2o × ( 2o ↑m 𝐴 ) ) )
35 34 ensymd ⊢ ( 𝐴 ∈ ω → ( 2o × ( 2o ↑m 𝐴 ) ) ≈ ( 2o × 𝒫 𝐴 ) )
36 entr ⊢ ( ( ( 2o ↑m suc 𝐴 ) ≈ ( 2o × ( 2o ↑m 𝐴 ) ) ∧ ( 2o × ( 2o ↑m 𝐴 ) ) ≈ ( 2o × 𝒫 𝐴 ) ) → ( 2o ↑m suc 𝐴 ) ≈ ( 2o × 𝒫 𝐴 ) )
37 30 35 36 syl2anc ⊢ ( 𝐴 ∈ ω → ( 2o ↑m suc 𝐴 ) ≈ ( 2o × 𝒫 𝐴 ) )
38 entr ⊢ ( ( 𝒫 suc 𝐴 ≈ ( 2o ↑m suc 𝐴 ) ∧ ( 2o ↑m suc 𝐴 ) ≈ ( 2o × 𝒫 𝐴 ) ) → 𝒫 suc 𝐴 ≈ ( 2o × 𝒫 𝐴 ) )
39 3 37 38 syl2anc ⊢ ( 𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ ( 2o × 𝒫 𝐴 ) )
40 xp2dju ⊢ ( 2o × 𝒫 𝐴 ) = ( 𝒫 𝐴 ⊔ 𝒫 𝐴 )
41 39 40 breqtrdi ⊢ ( 𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) )
42 nnfi ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ Fin )
43 pwfi ⊢ ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )
44 42 43 sylib ⊢ ( 𝐴 ∈ ω → 𝒫 𝐴 ∈ Fin )
45 ficardid ⊢ ( 𝒫 𝐴 ∈ Fin → ( card ‘ 𝒫 𝐴 ) ≈ 𝒫 𝐴 )
46 44 45 syl ⊢ ( 𝐴 ∈ ω → ( card ‘ 𝒫 𝐴 ) ≈ 𝒫 𝐴 )
47 djuen ⊢ ( ( ( card ‘ 𝒫 𝐴 ) ≈ 𝒫 𝐴 ∧ ( card ‘ 𝒫 𝐴 ) ≈ 𝒫 𝐴 ) → ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ≈ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) )
48 46 46 47 syl2anc ⊢ ( 𝐴 ∈ ω → ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ≈ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) )
49 48 ensymd ⊢ ( 𝐴 ∈ ω → ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) )
50 entr ⊢ ( ( 𝒫 suc 𝐴 ≈ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ∧ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ) → 𝒫 suc 𝐴 ≈ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) )
51 41 49 50 syl2anc ⊢ ( 𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) )
52 carden2b ⊢ ( 𝒫 suc 𝐴 ≈ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) → ( card ‘ 𝒫 suc 𝐴 ) = ( card ‘ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ) )
53 51 52 syl ⊢ ( 𝐴 ∈ ω → ( card ‘ 𝒫 suc 𝐴 ) = ( card ‘ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ) )
54 ficardom ⊢ ( 𝒫 𝐴 ∈ Fin → ( card ‘ 𝒫 𝐴 ) ∈ ω )
55 44 54 syl ⊢ ( 𝐴 ∈ ω → ( card ‘ 𝒫 𝐴 ) ∈ ω )
56 nnadju ⊢ ( ( ( card ‘ 𝒫 𝐴 ) ∈ ω ∧ ( card ‘ 𝒫 𝐴 ) ∈ ω ) → ( card ‘ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ) = ( ( card ‘ 𝒫 𝐴 ) +o ( card ‘ 𝒫 𝐴 ) ) )
57 55 55 56 syl2anc ⊢ ( 𝐴 ∈ ω → ( card ‘ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ) = ( ( card ‘ 𝒫 𝐴 ) +o ( card ‘ 𝒫 𝐴 ) ) )
58 53 57 eqtrd ⊢ ( 𝐴 ∈ ω → ( card ‘ 𝒫 suc 𝐴 ) = ( ( card ‘ 𝒫 𝐴 ) +o ( card ‘ 𝒫 𝐴 ) ) )