Proof of Theorem gchcdaidm
Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ∈ GCH) |
2 | | cdadom3 8893 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ 𝐴 ∈ GCH) → 𝐴 ≼ (𝐴 +𝑐 𝐴)) |
3 | 1, 1, 2 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≼ (𝐴 +𝑐 𝐴)) |
4 | | canth2g 7999 |
. . . . . . . . 9
⊢ (𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴) |
5 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≺ 𝒫 𝐴) |
6 | | sdomdom 7869 |
. . . . . . . 8
⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≼ 𝒫 𝐴) |
8 | | cdadom1 8891 |
. . . . . . . 8
⊢ (𝐴 ≼ 𝒫 𝐴 → (𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝐴)) |
9 | | cdadom2 8892 |
. . . . . . . 8
⊢ (𝐴 ≼ 𝒫 𝐴 → (𝒫 𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴)) |
10 | | domtr 7895 |
. . . . . . . 8
⊢ (((𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝐴) ∧ (𝒫 𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴)) → (𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴)) |
11 | 8, 9, 10 | syl2anc 691 |
. . . . . . 7
⊢ (𝐴 ≼ 𝒫 𝐴 → (𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝒫 𝐴)) |
12 | 7, 11 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴)) |
13 | | pwcda1 8899 |
. . . . . . . 8
⊢ (𝐴 ∈ GCH → (𝒫
𝐴 +𝑐
𝒫 𝐴) ≈
𝒫 (𝐴
+𝑐 1𝑜)) |
14 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝒫
𝐴 +𝑐
𝒫 𝐴) ≈
𝒫 (𝐴
+𝑐 1𝑜)) |
15 | | gchcda1 9357 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐
1𝑜) ≈ 𝐴) |
16 | | pwen 8018 |
. . . . . . . 8
⊢ ((𝐴 +𝑐
1𝑜) ≈ 𝐴 → 𝒫 (𝐴 +𝑐
1𝑜) ≈ 𝒫 𝐴) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝒫
(𝐴 +𝑐
1𝑜) ≈ 𝒫 𝐴) |
18 | | entr 7894 |
. . . . . . 7
⊢
(((𝒫 𝐴
+𝑐 𝒫 𝐴) ≈ 𝒫 (𝐴 +𝑐
1𝑜) ∧ 𝒫 (𝐴 +𝑐
1𝑜) ≈ 𝒫 𝐴) → (𝒫 𝐴 +𝑐 𝒫 𝐴) ≈ 𝒫 𝐴) |
19 | 14, 17, 18 | syl2anc 691 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝒫
𝐴 +𝑐
𝒫 𝐴) ≈
𝒫 𝐴) |
20 | | domentr 7901 |
. . . . . 6
⊢ (((𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴) ∧ (𝒫 𝐴 +𝑐 𝒫
𝐴) ≈ 𝒫 𝐴) → (𝐴 +𝑐 𝐴) ≼ 𝒫 𝐴) |
21 | 12, 19, 20 | syl2anc 691 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐 𝐴) ≼ 𝒫 𝐴) |
22 | | gchinf 9358 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ω
≼ 𝐴) |
23 | | pwcdandom 9368 |
. . . . . . 7
⊢ (ω
≼ 𝐴 → ¬
𝒫 𝐴 ≼ (𝐴 +𝑐 𝐴)) |
24 | 22, 23 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ¬
𝒫 𝐴 ≼ (𝐴 +𝑐 𝐴)) |
25 | | ensym 7891 |
. . . . . . 7
⊢ ((𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≈ (𝐴 +𝑐 𝐴)) |
26 | | endom 7868 |
. . . . . . 7
⊢
(𝒫 𝐴 ≈
(𝐴 +𝑐
𝐴) → 𝒫 𝐴 ≼ (𝐴 +𝑐 𝐴)) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ ((𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≼ (𝐴 +𝑐 𝐴)) |
28 | 24, 27 | nsyl 134 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ¬ (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴) |
29 | | brsdom 7864 |
. . . . 5
⊢ ((𝐴 +𝑐 𝐴) ≺ 𝒫 𝐴 ↔ ((𝐴 +𝑐 𝐴) ≼ 𝒫 𝐴 ∧ ¬ (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴)) |
30 | 21, 28, 29 | sylanbrc 695 |
. . . 4
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐 𝐴) ≺ 𝒫 𝐴) |
31 | 3, 30 | jca 553 |
. . 3
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ≼ (𝐴 +𝑐 𝐴) ∧ (𝐴 +𝑐 𝐴) ≺ 𝒫 𝐴)) |
32 | | gchen1 9326 |
. . 3
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ (𝐴 +𝑐 𝐴) ∧ (𝐴 +𝑐 𝐴) ≺ 𝒫 𝐴)) → 𝐴 ≈ (𝐴 +𝑐 𝐴)) |
33 | 31, 32 | mpdan 699 |
. 2
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≈ (𝐴 +𝑐 𝐴)) |
34 | 33 | ensymd 7893 |
1
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐 𝐴) ≈ 𝐴) |