Proof of Theorem gchcdaidm
Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ∈ GCH) |
2 | | cdadom3 9010 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ 𝐴 ∈ GCH) → 𝐴 ≼ (𝐴 +𝑐 𝐴)) |
3 | 1, 1, 2 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≼ (𝐴 +𝑐 𝐴)) |
4 | | canth2g 8114 |
. . . . . . . . 9
⊢ (𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴) |
5 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≺ 𝒫 𝐴) |
6 | | sdomdom 7983 |
. . . . . . . 8
⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≼ 𝒫 𝐴) |
8 | | cdadom1 9008 |
. . . . . . . 8
⊢ (𝐴 ≼ 𝒫 𝐴 → (𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝐴)) |
9 | | cdadom2 9009 |
. . . . . . . 8
⊢ (𝐴 ≼ 𝒫 𝐴 → (𝒫 𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴)) |
10 | | domtr 8009 |
. . . . . . . 8
⊢ (((𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝐴) ∧ (𝒫 𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴)) → (𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴)) |
11 | 8, 9, 10 | syl2anc 693 |
. . . . . . 7
⊢ (𝐴 ≼ 𝒫 𝐴 → (𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝒫 𝐴)) |
12 | 7, 11 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴)) |
13 | | pwcda1 9016 |
. . . . . . . 8
⊢ (𝐴 ∈ GCH → (𝒫
𝐴 +𝑐
𝒫 𝐴) ≈
𝒫 (𝐴
+𝑐 1𝑜)) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝒫
𝐴 +𝑐
𝒫 𝐴) ≈
𝒫 (𝐴
+𝑐 1𝑜)) |
15 | | gchcda1 9478 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐
1𝑜) ≈ 𝐴) |
16 | | pwen 8133 |
. . . . . . . 8
⊢ ((𝐴 +𝑐
1𝑜) ≈ 𝐴 → 𝒫 (𝐴 +𝑐
1𝑜) ≈ 𝒫 𝐴) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝒫
(𝐴 +𝑐
1𝑜) ≈ 𝒫 𝐴) |
18 | | entr 8008 |
. . . . . . 7
⊢
(((𝒫 𝐴
+𝑐 𝒫 𝐴) ≈ 𝒫 (𝐴 +𝑐
1𝑜) ∧ 𝒫 (𝐴 +𝑐
1𝑜) ≈ 𝒫 𝐴) → (𝒫 𝐴 +𝑐 𝒫 𝐴) ≈ 𝒫 𝐴) |
19 | 14, 17, 18 | syl2anc 693 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝒫
𝐴 +𝑐
𝒫 𝐴) ≈
𝒫 𝐴) |
20 | | domentr 8015 |
. . . . . 6
⊢ (((𝐴 +𝑐 𝐴) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴) ∧ (𝒫 𝐴 +𝑐 𝒫
𝐴) ≈ 𝒫 𝐴) → (𝐴 +𝑐 𝐴) ≼ 𝒫 𝐴) |
21 | 12, 19, 20 | syl2anc 693 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐 𝐴) ≼ 𝒫 𝐴) |
22 | | gchinf 9479 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ω
≼ 𝐴) |
23 | | pwcdandom 9489 |
. . . . . . 7
⊢ (ω
≼ 𝐴 → ¬
𝒫 𝐴 ≼ (𝐴 +𝑐 𝐴)) |
24 | 22, 23 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ¬
𝒫 𝐴 ≼ (𝐴 +𝑐 𝐴)) |
25 | | ensym 8005 |
. . . . . . 7
⊢ ((𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≈ (𝐴 +𝑐 𝐴)) |
26 | | endom 7982 |
. . . . . . 7
⊢
(𝒫 𝐴 ≈
(𝐴 +𝑐
𝐴) → 𝒫 𝐴 ≼ (𝐴 +𝑐 𝐴)) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ ((𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≼ (𝐴 +𝑐 𝐴)) |
28 | 24, 27 | nsyl 135 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ¬ (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴) |
29 | | brsdom 7978 |
. . . . 5
⊢ ((𝐴 +𝑐 𝐴) ≺ 𝒫 𝐴 ↔ ((𝐴 +𝑐 𝐴) ≼ 𝒫 𝐴 ∧ ¬ (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴)) |
30 | 21, 28, 29 | sylanbrc 698 |
. . . 4
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐 𝐴) ≺ 𝒫 𝐴) |
31 | 3, 30 | jca 554 |
. . 3
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ≼ (𝐴 +𝑐 𝐴) ∧ (𝐴 +𝑐 𝐴) ≺ 𝒫 𝐴)) |
32 | | gchen1 9447 |
. . 3
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ (𝐴 +𝑐 𝐴) ∧ (𝐴 +𝑐 𝐴) ≺ 𝒫 𝐴)) → 𝐴 ≈ (𝐴 +𝑐 𝐴)) |
33 | 31, 32 | mpdan 702 |
. 2
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≈ (𝐴 +𝑐 𝐴)) |
34 | 33 | ensymd 8007 |
1
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐 𝐴) ≈ 𝐴) |