Step | Hyp | Ref
| Expression |
1 | | suceq 5790 |
. . . . 5
⊢ (𝑎 = 𝐴 → suc 𝑎 = suc 𝐴) |
2 | 1 | pweqd 4163 |
. . . 4
⊢ (𝑎 = 𝐴 → 𝒫 suc 𝑎 = 𝒫 suc 𝐴) |
3 | 2 | fveq2d 6195 |
. . 3
⊢ (𝑎 = 𝐴 → (card‘𝒫 suc 𝑎) = (card‘𝒫 suc
𝐴)) |
4 | | pweq 4161 |
. . . . 5
⊢ (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴) |
5 | 4 | fveq2d 6195 |
. . . 4
⊢ (𝑎 = 𝐴 → (card‘𝒫 𝑎) = (card‘𝒫 𝐴)) |
6 | 5, 5 | oveq12d 6668 |
. . 3
⊢ (𝑎 = 𝐴 → ((card‘𝒫 𝑎) +𝑜
(card‘𝒫 𝑎)) =
((card‘𝒫 𝐴)
+𝑜 (card‘𝒫 𝐴))) |
7 | 3, 6 | eqeq12d 2637 |
. 2
⊢ (𝑎 = 𝐴 → ((card‘𝒫 suc 𝑎) = ((card‘𝒫 𝑎) +𝑜
(card‘𝒫 𝑎))
↔ (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +𝑜
(card‘𝒫 𝐴)))) |
8 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
9 | 8 | sucex 7011 |
. . . . . . . 8
⊢ suc 𝑎 ∈ V |
10 | 9 | pw2en 8067 |
. . . . . . 7
⊢ 𝒫
suc 𝑎 ≈
(2𝑜 ↑𝑚 suc 𝑎) |
11 | | df-suc 5729 |
. . . . . . . . . 10
⊢ suc 𝑎 = (𝑎 ∪ {𝑎}) |
12 | 11 | oveq2i 6661 |
. . . . . . . . 9
⊢
(2𝑜 ↑𝑚 suc 𝑎) = (2𝑜
↑𝑚 (𝑎 ∪ {𝑎})) |
13 | | nnord 7073 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ω → Ord 𝑎) |
14 | | orddisj 5762 |
. . . . . . . . . . 11
⊢ (Ord
𝑎 → (𝑎 ∩ {𝑎}) = ∅) |
15 | | snex 4908 |
. . . . . . . . . . . 12
⊢ {𝑎} ∈ V |
16 | | 2onn 7720 |
. . . . . . . . . . . . 13
⊢
2𝑜 ∈ ω |
17 | 16 | elexi 3213 |
. . . . . . . . . . . 12
⊢
2𝑜 ∈ V |
18 | | mapunen 8129 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ V ∧ {𝑎} ∈ V ∧
2𝑜 ∈ V) ∧ (𝑎 ∩ {𝑎}) = ∅) → (2𝑜
↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎}))) |
19 | 18 | ex 450 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ V ∧ {𝑎} ∈ V ∧
2𝑜 ∈ V) → ((𝑎 ∩ {𝑎}) = ∅ → (2𝑜
↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎})))) |
20 | 8, 15, 17, 19 | mp3an 1424 |
. . . . . . . . . . 11
⊢ ((𝑎 ∩ {𝑎}) = ∅ → (2𝑜
↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎}))) |
21 | 13, 14, 20 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ω →
(2𝑜 ↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎}))) |
22 | | ovex 6678 |
. . . . . . . . . . . 12
⊢
(2𝑜 ↑𝑚 𝑎) ∈ V |
23 | 22 | enref 7988 |
. . . . . . . . . . 11
⊢
(2𝑜 ↑𝑚 𝑎) ≈ (2𝑜
↑𝑚 𝑎) |
24 | 17, 8 | mapsnen 8035 |
. . . . . . . . . . 11
⊢
(2𝑜 ↑𝑚 {𝑎}) ≈
2𝑜 |
25 | | xpen 8123 |
. . . . . . . . . . 11
⊢
(((2𝑜 ↑𝑚 𝑎) ≈ (2𝑜
↑𝑚 𝑎) ∧ (2𝑜
↑𝑚 {𝑎}) ≈ 2𝑜) →
((2𝑜 ↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) ×
2𝑜)) |
26 | 23, 24, 25 | mp2an 708 |
. . . . . . . . . 10
⊢
((2𝑜 ↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) ×
2𝑜) |
27 | | entr 8008 |
. . . . . . . . . 10
⊢
(((2𝑜 ↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎})) ∧ ((2𝑜
↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) × 2𝑜)) →
(2𝑜 ↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) ×
2𝑜)) |
28 | 21, 26, 27 | sylancl 694 |
. . . . . . . . 9
⊢ (𝑎 ∈ ω →
(2𝑜 ↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) ×
2𝑜)) |
29 | 12, 28 | syl5eqbr 4688 |
. . . . . . . 8
⊢ (𝑎 ∈ ω →
(2𝑜 ↑𝑚 suc 𝑎) ≈ ((2𝑜
↑𝑚 𝑎) ×
2𝑜)) |
30 | 8 | pw2en 8067 |
. . . . . . . . . 10
⊢ 𝒫
𝑎 ≈
(2𝑜 ↑𝑚 𝑎) |
31 | 17 | enref 7988 |
. . . . . . . . . 10
⊢
2𝑜 ≈ 2𝑜 |
32 | | xpen 8123 |
. . . . . . . . . 10
⊢
((𝒫 𝑎
≈ (2𝑜 ↑𝑚 𝑎) ∧ 2𝑜 ≈
2𝑜) → (𝒫 𝑎 × 2𝑜) ≈
((2𝑜 ↑𝑚 𝑎) ×
2𝑜)) |
33 | 30, 31, 32 | mp2an 708 |
. . . . . . . . 9
⊢
(𝒫 𝑎 ×
2𝑜) ≈ ((2𝑜
↑𝑚 𝑎) ×
2𝑜) |
34 | 33 | ensymi 8006 |
. . . . . . . 8
⊢
((2𝑜 ↑𝑚 𝑎) × 2𝑜) ≈
(𝒫 𝑎 ×
2𝑜) |
35 | | entr 8008 |
. . . . . . . 8
⊢
(((2𝑜 ↑𝑚 suc 𝑎) ≈
((2𝑜 ↑𝑚 𝑎) × 2𝑜) ∧
((2𝑜 ↑𝑚 𝑎) × 2𝑜) ≈
(𝒫 𝑎 ×
2𝑜)) → (2𝑜
↑𝑚 suc 𝑎) ≈ (𝒫 𝑎 ×
2𝑜)) |
36 | 29, 34, 35 | sylancl 694 |
. . . . . . 7
⊢ (𝑎 ∈ ω →
(2𝑜 ↑𝑚 suc 𝑎) ≈ (𝒫 𝑎 ×
2𝑜)) |
37 | | entr 8008 |
. . . . . . 7
⊢
((𝒫 suc 𝑎
≈ (2𝑜 ↑𝑚 suc 𝑎) ∧ (2𝑜
↑𝑚 suc 𝑎) ≈ (𝒫 𝑎 × 2𝑜)) →
𝒫 suc 𝑎 ≈
(𝒫 𝑎 ×
2𝑜)) |
38 | 10, 36, 37 | sylancr 695 |
. . . . . 6
⊢ (𝑎 ∈ ω → 𝒫
suc 𝑎 ≈ (𝒫
𝑎 ×
2𝑜)) |
39 | | vpwex 4849 |
. . . . . . 7
⊢ 𝒫
𝑎 ∈ V |
40 | | xp2cda 9002 |
. . . . . . 7
⊢
(𝒫 𝑎 ∈
V → (𝒫 𝑎
× 2𝑜) = (𝒫 𝑎 +𝑐 𝒫 𝑎)) |
41 | 39, 40 | ax-mp 5 |
. . . . . 6
⊢
(𝒫 𝑎 ×
2𝑜) = (𝒫 𝑎 +𝑐 𝒫 𝑎) |
42 | 38, 41 | syl6breq 4694 |
. . . . 5
⊢ (𝑎 ∈ ω → 𝒫
suc 𝑎 ≈ (𝒫
𝑎 +𝑐
𝒫 𝑎)) |
43 | | nnfi 8153 |
. . . . . . . . 9
⊢ (𝑎 ∈ ω → 𝑎 ∈ Fin) |
44 | | pwfi 8261 |
. . . . . . . . 9
⊢ (𝑎 ∈ Fin ↔ 𝒫
𝑎 ∈
Fin) |
45 | 43, 44 | sylib 208 |
. . . . . . . 8
⊢ (𝑎 ∈ ω → 𝒫
𝑎 ∈
Fin) |
46 | | ficardid 8788 |
. . . . . . . 8
⊢
(𝒫 𝑎 ∈
Fin → (card‘𝒫 𝑎) ≈ 𝒫 𝑎) |
47 | 45, 46 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ ω →
(card‘𝒫 𝑎)
≈ 𝒫 𝑎) |
48 | | cdaen 8995 |
. . . . . . 7
⊢
(((card‘𝒫 𝑎) ≈ 𝒫 𝑎 ∧ (card‘𝒫 𝑎) ≈ 𝒫 𝑎) → ((card‘𝒫
𝑎) +𝑐
(card‘𝒫 𝑎))
≈ (𝒫 𝑎
+𝑐 𝒫 𝑎)) |
49 | 47, 47, 48 | syl2anc 693 |
. . . . . 6
⊢ (𝑎 ∈ ω →
((card‘𝒫 𝑎)
+𝑐 (card‘𝒫 𝑎)) ≈ (𝒫 𝑎 +𝑐 𝒫 𝑎)) |
50 | 49 | ensymd 8007 |
. . . . 5
⊢ (𝑎 ∈ ω →
(𝒫 𝑎
+𝑐 𝒫 𝑎) ≈ ((card‘𝒫 𝑎) +𝑐
(card‘𝒫 𝑎))) |
51 | | entr 8008 |
. . . . 5
⊢
((𝒫 suc 𝑎
≈ (𝒫 𝑎
+𝑐 𝒫 𝑎) ∧ (𝒫 𝑎 +𝑐 𝒫 𝑎) ≈ ((card‘𝒫
𝑎) +𝑐
(card‘𝒫 𝑎)))
→ 𝒫 suc 𝑎
≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫
𝑎))) |
52 | 42, 50, 51 | syl2anc 693 |
. . . 4
⊢ (𝑎 ∈ ω → 𝒫
suc 𝑎 ≈
((card‘𝒫 𝑎)
+𝑐 (card‘𝒫 𝑎))) |
53 | | carden2b 8793 |
. . . 4
⊢
(𝒫 suc 𝑎
≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫
𝑎)) →
(card‘𝒫 suc 𝑎) = (card‘((card‘𝒫 𝑎) +𝑐
(card‘𝒫 𝑎)))) |
54 | 52, 53 | syl 17 |
. . 3
⊢ (𝑎 ∈ ω →
(card‘𝒫 suc 𝑎) = (card‘((card‘𝒫 𝑎) +𝑐
(card‘𝒫 𝑎)))) |
55 | | ficardom 8787 |
. . . . 5
⊢
(𝒫 𝑎 ∈
Fin → (card‘𝒫 𝑎) ∈ ω) |
56 | 45, 55 | syl 17 |
. . . 4
⊢ (𝑎 ∈ ω →
(card‘𝒫 𝑎)
∈ ω) |
57 | | nnacda 9023 |
. . . 4
⊢
(((card‘𝒫 𝑎) ∈ ω ∧ (card‘𝒫
𝑎) ∈ ω) →
(card‘((card‘𝒫 𝑎) +𝑐 (card‘𝒫
𝑎))) =
((card‘𝒫 𝑎)
+𝑜 (card‘𝒫 𝑎))) |
58 | 56, 56, 57 | syl2anc 693 |
. . 3
⊢ (𝑎 ∈ ω →
(card‘((card‘𝒫 𝑎) +𝑐 (card‘𝒫
𝑎))) =
((card‘𝒫 𝑎)
+𝑜 (card‘𝒫 𝑎))) |
59 | 54, 58 | eqtrd 2656 |
. 2
⊢ (𝑎 ∈ ω →
(card‘𝒫 suc 𝑎) = ((card‘𝒫 𝑎) +𝑜 (card‘𝒫
𝑎))) |
60 | 7, 59 | vtoclga 3272 |
1
⊢ (𝐴 ∈ ω →
(card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +𝑜
(card‘𝒫 𝐴))) |