Step | Hyp | Ref
| Expression |
1 | | suceq 5707 |
. . . . 5
⊢ (𝑎 = 𝐴 → suc 𝑎 = suc 𝐴) |
2 | 1 | pweqd 4113 |
. . . 4
⊢ (𝑎 = 𝐴 → 𝒫 suc 𝑎 = 𝒫 suc 𝐴) |
3 | 2 | fveq2d 6107 |
. . 3
⊢ (𝑎 = 𝐴 → (card‘𝒫 suc 𝑎) = (card‘𝒫 suc
𝐴)) |
4 | | pweq 4111 |
. . . . 5
⊢ (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴) |
5 | 4 | fveq2d 6107 |
. . . 4
⊢ (𝑎 = 𝐴 → (card‘𝒫 𝑎) = (card‘𝒫 𝐴)) |
6 | 5, 5 | oveq12d 6567 |
. . 3
⊢ (𝑎 = 𝐴 → ((card‘𝒫 𝑎) +𝑜
(card‘𝒫 𝑎)) =
((card‘𝒫 𝐴)
+𝑜 (card‘𝒫 𝐴))) |
7 | 3, 6 | eqeq12d 2625 |
. 2
⊢ (𝑎 = 𝐴 → ((card‘𝒫 suc 𝑎) = ((card‘𝒫 𝑎) +𝑜
(card‘𝒫 𝑎))
↔ (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +𝑜
(card‘𝒫 𝐴)))) |
8 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
9 | 8 | sucex 6903 |
. . . . . . . 8
⊢ suc 𝑎 ∈ V |
10 | 9 | pw2en 7952 |
. . . . . . 7
⊢ 𝒫
suc 𝑎 ≈
(2𝑜 ↑𝑚 suc 𝑎) |
11 | | df-suc 5646 |
. . . . . . . . . 10
⊢ suc 𝑎 = (𝑎 ∪ {𝑎}) |
12 | 11 | oveq2i 6560 |
. . . . . . . . 9
⊢
(2𝑜 ↑𝑚 suc 𝑎) = (2𝑜
↑𝑚 (𝑎 ∪ {𝑎})) |
13 | | nnord 6965 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ω → Ord 𝑎) |
14 | | orddisj 5679 |
. . . . . . . . . . 11
⊢ (Ord
𝑎 → (𝑎 ∩ {𝑎}) = ∅) |
15 | | snex 4835 |
. . . . . . . . . . . 12
⊢ {𝑎} ∈ V |
16 | | 2onn 7607 |
. . . . . . . . . . . . 13
⊢
2𝑜 ∈ ω |
17 | 16 | elexi 3186 |
. . . . . . . . . . . 12
⊢
2𝑜 ∈ V |
18 | | mapunen 8014 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ V ∧ {𝑎} ∈ V ∧
2𝑜 ∈ V) ∧ (𝑎 ∩ {𝑎}) = ∅) → (2𝑜
↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎}))) |
19 | 18 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ V ∧ {𝑎} ∈ V ∧
2𝑜 ∈ V) → ((𝑎 ∩ {𝑎}) = ∅ → (2𝑜
↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎})))) |
20 | 8, 15, 17, 19 | mp3an 1416 |
. . . . . . . . . . 11
⊢ ((𝑎 ∩ {𝑎}) = ∅ → (2𝑜
↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎}))) |
21 | 13, 14, 20 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ω →
(2𝑜 ↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎}))) |
22 | | ovex 6577 |
. . . . . . . . . . . 12
⊢
(2𝑜 ↑𝑚 𝑎) ∈ V |
23 | 22 | enref 7874 |
. . . . . . . . . . 11
⊢
(2𝑜 ↑𝑚 𝑎) ≈ (2𝑜
↑𝑚 𝑎) |
24 | 17, 8 | mapsnen 7920 |
. . . . . . . . . . 11
⊢
(2𝑜 ↑𝑚 {𝑎}) ≈
2𝑜 |
25 | | xpen 8008 |
. . . . . . . . . . 11
⊢
(((2𝑜 ↑𝑚 𝑎) ≈ (2𝑜
↑𝑚 𝑎) ∧ (2𝑜
↑𝑚 {𝑎}) ≈ 2𝑜) →
((2𝑜 ↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) ×
2𝑜)) |
26 | 23, 24, 25 | mp2an 704 |
. . . . . . . . . 10
⊢
((2𝑜 ↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) ×
2𝑜) |
27 | | entr 7894 |
. . . . . . . . . 10
⊢
(((2𝑜 ↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎})) ∧ ((2𝑜
↑𝑚 𝑎) × (2𝑜
↑𝑚 {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) × 2𝑜)) →
(2𝑜 ↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) ×
2𝑜)) |
28 | 21, 26, 27 | sylancl 693 |
. . . . . . . . 9
⊢ (𝑎 ∈ ω →
(2𝑜 ↑𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜
↑𝑚 𝑎) ×
2𝑜)) |
29 | 12, 28 | syl5eqbr 4618 |
. . . . . . . 8
⊢ (𝑎 ∈ ω →
(2𝑜 ↑𝑚 suc 𝑎) ≈ ((2𝑜
↑𝑚 𝑎) ×
2𝑜)) |
30 | 8 | pw2en 7952 |
. . . . . . . . . 10
⊢ 𝒫
𝑎 ≈
(2𝑜 ↑𝑚 𝑎) |
31 | 17 | enref 7874 |
. . . . . . . . . 10
⊢
2𝑜 ≈ 2𝑜 |
32 | | xpen 8008 |
. . . . . . . . . 10
⊢
((𝒫 𝑎
≈ (2𝑜 ↑𝑚 𝑎) ∧ 2𝑜 ≈
2𝑜) → (𝒫 𝑎 × 2𝑜) ≈
((2𝑜 ↑𝑚 𝑎) ×
2𝑜)) |
33 | 30, 31, 32 | mp2an 704 |
. . . . . . . . 9
⊢
(𝒫 𝑎 ×
2𝑜) ≈ ((2𝑜
↑𝑚 𝑎) ×
2𝑜) |
34 | 33 | ensymi 7892 |
. . . . . . . 8
⊢
((2𝑜 ↑𝑚 𝑎) × 2𝑜) ≈
(𝒫 𝑎 ×
2𝑜) |
35 | | entr 7894 |
. . . . . . . 8
⊢
(((2𝑜 ↑𝑚 suc 𝑎) ≈
((2𝑜 ↑𝑚 𝑎) × 2𝑜) ∧
((2𝑜 ↑𝑚 𝑎) × 2𝑜) ≈
(𝒫 𝑎 ×
2𝑜)) → (2𝑜
↑𝑚 suc 𝑎) ≈ (𝒫 𝑎 ×
2𝑜)) |
36 | 29, 34, 35 | sylancl 693 |
. . . . . . 7
⊢ (𝑎 ∈ ω →
(2𝑜 ↑𝑚 suc 𝑎) ≈ (𝒫 𝑎 ×
2𝑜)) |
37 | | entr 7894 |
. . . . . . 7
⊢
((𝒫 suc 𝑎
≈ (2𝑜 ↑𝑚 suc 𝑎) ∧ (2𝑜
↑𝑚 suc 𝑎) ≈ (𝒫 𝑎 × 2𝑜)) →
𝒫 suc 𝑎 ≈
(𝒫 𝑎 ×
2𝑜)) |
38 | 10, 36, 37 | sylancr 694 |
. . . . . 6
⊢ (𝑎 ∈ ω → 𝒫
suc 𝑎 ≈ (𝒫
𝑎 ×
2𝑜)) |
39 | | vpwex 4775 |
. . . . . . 7
⊢ 𝒫
𝑎 ∈ V |
40 | | xp2cda 8885 |
. . . . . . 7
⊢
(𝒫 𝑎 ∈
V → (𝒫 𝑎
× 2𝑜) = (𝒫 𝑎 +𝑐 𝒫 𝑎)) |
41 | 39, 40 | ax-mp 5 |
. . . . . 6
⊢
(𝒫 𝑎 ×
2𝑜) = (𝒫 𝑎 +𝑐 𝒫 𝑎) |
42 | 38, 41 | syl6breq 4624 |
. . . . 5
⊢ (𝑎 ∈ ω → 𝒫
suc 𝑎 ≈ (𝒫
𝑎 +𝑐
𝒫 𝑎)) |
43 | | nnfi 8038 |
. . . . . . . . 9
⊢ (𝑎 ∈ ω → 𝑎 ∈ Fin) |
44 | | pwfi 8144 |
. . . . . . . . 9
⊢ (𝑎 ∈ Fin ↔ 𝒫
𝑎 ∈
Fin) |
45 | 43, 44 | sylib 207 |
. . . . . . . 8
⊢ (𝑎 ∈ ω → 𝒫
𝑎 ∈
Fin) |
46 | | ficardid 8671 |
. . . . . . . 8
⊢
(𝒫 𝑎 ∈
Fin → (card‘𝒫 𝑎) ≈ 𝒫 𝑎) |
47 | 45, 46 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ ω →
(card‘𝒫 𝑎)
≈ 𝒫 𝑎) |
48 | | cdaen 8878 |
. . . . . . 7
⊢
(((card‘𝒫 𝑎) ≈ 𝒫 𝑎 ∧ (card‘𝒫 𝑎) ≈ 𝒫 𝑎) → ((card‘𝒫
𝑎) +𝑐
(card‘𝒫 𝑎))
≈ (𝒫 𝑎
+𝑐 𝒫 𝑎)) |
49 | 47, 47, 48 | syl2anc 691 |
. . . . . 6
⊢ (𝑎 ∈ ω →
((card‘𝒫 𝑎)
+𝑐 (card‘𝒫 𝑎)) ≈ (𝒫 𝑎 +𝑐 𝒫 𝑎)) |
50 | 49 | ensymd 7893 |
. . . . 5
⊢ (𝑎 ∈ ω →
(𝒫 𝑎
+𝑐 𝒫 𝑎) ≈ ((card‘𝒫 𝑎) +𝑐
(card‘𝒫 𝑎))) |
51 | | entr 7894 |
. . . . 5
⊢
((𝒫 suc 𝑎
≈ (𝒫 𝑎
+𝑐 𝒫 𝑎) ∧ (𝒫 𝑎 +𝑐 𝒫 𝑎) ≈ ((card‘𝒫
𝑎) +𝑐
(card‘𝒫 𝑎)))
→ 𝒫 suc 𝑎
≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫
𝑎))) |
52 | 42, 50, 51 | syl2anc 691 |
. . . 4
⊢ (𝑎 ∈ ω → 𝒫
suc 𝑎 ≈
((card‘𝒫 𝑎)
+𝑐 (card‘𝒫 𝑎))) |
53 | | carden2b 8676 |
. . . 4
⊢
(𝒫 suc 𝑎
≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫
𝑎)) →
(card‘𝒫 suc 𝑎) = (card‘((card‘𝒫 𝑎) +𝑐
(card‘𝒫 𝑎)))) |
54 | 52, 53 | syl 17 |
. . 3
⊢ (𝑎 ∈ ω →
(card‘𝒫 suc 𝑎) = (card‘((card‘𝒫 𝑎) +𝑐
(card‘𝒫 𝑎)))) |
55 | | ficardom 8670 |
. . . . 5
⊢
(𝒫 𝑎 ∈
Fin → (card‘𝒫 𝑎) ∈ ω) |
56 | 45, 55 | syl 17 |
. . . 4
⊢ (𝑎 ∈ ω →
(card‘𝒫 𝑎)
∈ ω) |
57 | | nnacda 8906 |
. . . 4
⊢
(((card‘𝒫 𝑎) ∈ ω ∧ (card‘𝒫
𝑎) ∈ ω) →
(card‘((card‘𝒫 𝑎) +𝑐 (card‘𝒫
𝑎))) =
((card‘𝒫 𝑎)
+𝑜 (card‘𝒫 𝑎))) |
58 | 56, 56, 57 | syl2anc 691 |
. . 3
⊢ (𝑎 ∈ ω →
(card‘((card‘𝒫 𝑎) +𝑐 (card‘𝒫
𝑎))) =
((card‘𝒫 𝑎)
+𝑜 (card‘𝒫 𝑎))) |
59 | 54, 58 | eqtrd 2644 |
. 2
⊢ (𝑎 ∈ ω →
(card‘𝒫 suc 𝑎) = ((card‘𝒫 𝑎) +𝑜 (card‘𝒫
𝑎))) |
60 | 7, 59 | vtoclga 3245 |
1
⊢ (𝐴 ∈ ω →
(card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +𝑜
(card‘𝒫 𝐴))) |