Proof of Theorem gchhar
Step | Hyp | Ref
| Expression |
1 | | harcl 8349 |
. . . 4
⊢
(har‘𝐴) ∈
On |
2 | | simp3 1056 |
. . . 4
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ∈
GCH) |
3 | | cdadom3 8893 |
. . . 4
⊢
(((har‘𝐴)
∈ On ∧ 𝒫 𝐴
∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) +𝑐 𝒫 𝐴)) |
4 | 1, 2, 3 | sylancr 694 |
. . 3
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(har‘𝐴) ≼
((har‘𝐴)
+𝑐 𝒫 𝐴)) |
5 | | domnsym 7971 |
. . . . . . . . 9
⊢ (ω
≼ 𝐴 → ¬
𝐴 ≺
ω) |
6 | 5 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → ¬
𝐴 ≺
ω) |
7 | | isfinite 8432 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺
ω) |
8 | 6, 7 | sylnibr 318 |
. . . . . . 7
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → ¬
𝐴 ∈
Fin) |
9 | | pwfi 8144 |
. . . . . . 7
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
10 | 8, 9 | sylnib 317 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → ¬
𝒫 𝐴 ∈
Fin) |
11 | | cdadom3 8893 |
. . . . . . 7
⊢
((𝒫 𝐴 ∈
GCH ∧ (har‘𝐴)
∈ On) → 𝒫 𝐴 ≼ (𝒫 𝐴 +𝑐 (har‘𝐴))) |
12 | 2, 1, 11 | sylancl 693 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ≼
(𝒫 𝐴
+𝑐 (har‘𝐴))) |
13 | | ovex 6577 |
. . . . . . . 8
⊢
(𝒫 𝐴
+𝑐 (har‘𝐴)) ∈ V |
14 | 13 | canth2 7998 |
. . . . . . 7
⊢
(𝒫 𝐴
+𝑐 (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 +𝑐
(har‘𝐴)) |
15 | | pwcdaen 8890 |
. . . . . . . . 9
⊢
((𝒫 𝐴 ∈
GCH ∧ (har‘𝐴)
∈ On) → 𝒫 (𝒫 𝐴 +𝑐 (har‘𝐴)) ≈ (𝒫 𝒫
𝐴 × 𝒫
(har‘𝐴))) |
16 | 2, 1, 15 | sylancl 693 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝒫 𝐴
+𝑐 (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫
(har‘𝐴))) |
17 | | pwexg 4776 |
. . . . . . . . . . 11
⊢
(𝒫 𝐴 ∈
GCH → 𝒫 𝒫 𝐴 ∈ V) |
18 | 2, 17 | syl 17 |
. . . . . . . . . 10
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝒫 𝐴
∈ V) |
19 | | simp2 1055 |
. . . . . . . . . . 11
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → 𝐴 ∈ GCH) |
20 | | harwdom 8378 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ GCH →
(har‘𝐴)
≼* 𝒫 (𝐴 × 𝐴)) |
21 | | wdompwdom 8366 |
. . . . . . . . . . 11
⊢
((har‘𝐴)
≼* 𝒫 (𝐴 × 𝐴) → 𝒫 (har‘𝐴) ≼ 𝒫 𝒫
(𝐴 × 𝐴)) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . . 10
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (har‘𝐴)
≼ 𝒫 𝒫 (𝐴 × 𝐴)) |
23 | | xpdom2g 7941 |
. . . . . . . . . 10
⊢
((𝒫 𝒫 𝐴 ∈ V ∧ 𝒫 (har‘𝐴) ≼ 𝒫 𝒫
(𝐴 × 𝐴)) → (𝒫 𝒫
𝐴 × 𝒫
(har‘𝐴)) ≼
(𝒫 𝒫 𝐴
× 𝒫 𝒫 (𝐴 × 𝐴))) |
24 | 18, 22, 23 | syl2anc 691 |
. . . . . . . . 9
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝒫 𝐴
× 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫
(𝐴 × 𝐴))) |
25 | | xpexg 6858 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ GCH ∧ 𝐴 ∈ GCH) → (𝐴 × 𝐴) ∈ V) |
26 | 19, 19, 25 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 × 𝐴) ∈ V) |
27 | | pwexg 4776 |
. . . . . . . . . . . . 13
⊢ ((𝐴 × 𝐴) ∈ V → 𝒫 (𝐴 × 𝐴) ∈ V) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝐴 × 𝐴) ∈ V) |
29 | | pwcdaen 8890 |
. . . . . . . . . . . 12
⊢
((𝒫 𝐴 ∈
GCH ∧ 𝒫 (𝐴
× 𝐴) ∈ V) →
𝒫 (𝒫 𝐴
+𝑐 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 𝒫
(𝐴 × 𝐴))) |
30 | 2, 28, 29 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝒫 𝐴
+𝑐 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 𝒫
(𝐴 × 𝐴))) |
31 | 30 | ensymd 7893 |
. . . . . . . . . 10
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝒫 𝐴
× 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 (𝒫 𝐴 +𝑐 𝒫
(𝐴 × 𝐴))) |
32 | | enrefg 7873 |
. . . . . . . . . . . . . 14
⊢
(𝒫 𝐴 ∈
GCH → 𝒫 𝐴
≈ 𝒫 𝐴) |
33 | 2, 32 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ≈
𝒫 𝐴) |
34 | | gchxpidm 9370 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≈ 𝐴) |
35 | 19, 8, 34 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 × 𝐴) ≈ 𝐴) |
36 | | pwen 8018 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 × 𝐴) ≈ 𝐴 → 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴) |
38 | | cdaen 8878 |
. . . . . . . . . . . . 13
⊢
((𝒫 𝐴
≈ 𝒫 𝐴 ∧
𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴) → (𝒫 𝐴 +𝑐 𝒫
(𝐴 × 𝐴)) ≈ (𝒫 𝐴 +𝑐 𝒫
𝐴)) |
39 | 33, 37, 38 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝐴
+𝑐 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 +𝑐 𝒫 𝐴)) |
40 | | gchcdaidm 9369 |
. . . . . . . . . . . . 13
⊢
((𝒫 𝐴 ∈
GCH ∧ ¬ 𝒫 𝐴
∈ Fin) → (𝒫 𝐴 +𝑐 𝒫 𝐴) ≈ 𝒫 𝐴) |
41 | 2, 10, 40 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝐴
+𝑐 𝒫 𝐴) ≈ 𝒫 𝐴) |
42 | | entr 7894 |
. . . . . . . . . . . 12
⊢
(((𝒫 𝐴
+𝑐 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 +𝑐 𝒫 𝐴) ∧ (𝒫 𝐴 +𝑐 𝒫
𝐴) ≈ 𝒫 𝐴) → (𝒫 𝐴 +𝑐 𝒫
(𝐴 × 𝐴)) ≈ 𝒫 𝐴) |
43 | 39, 41, 42 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝐴
+𝑐 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴) |
44 | | pwen 8018 |
. . . . . . . . . . 11
⊢
((𝒫 𝐴
+𝑐 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴 → 𝒫 (𝒫 𝐴 +𝑐 𝒫
(𝐴 × 𝐴)) ≈ 𝒫 𝒫
𝐴) |
45 | 43, 44 | syl 17 |
. . . . . . . . . 10
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝒫 𝐴
+𝑐 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴) |
46 | | entr 7894 |
. . . . . . . . . 10
⊢
(((𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 (𝒫 𝐴 +𝑐 𝒫
(𝐴 × 𝐴)) ∧ 𝒫 (𝒫
𝐴 +𝑐
𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫
𝐴) → (𝒫
𝒫 𝐴 ×
𝒫 𝒫 (𝐴
× 𝐴)) ≈
𝒫 𝒫 𝐴) |
47 | 31, 45, 46 | syl2anc 691 |
. . . . . . . . 9
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝒫 𝐴
× 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴) |
48 | | domentr 7901 |
. . . . . . . . 9
⊢
(((𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫
𝐴 × 𝒫
𝒫 (𝐴 × 𝐴)) ∧ (𝒫 𝒫
𝐴 × 𝒫
𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫
𝐴) → (𝒫
𝒫 𝐴 ×
𝒫 (har‘𝐴))
≼ 𝒫 𝒫 𝐴) |
49 | 24, 47, 48 | syl2anc 691 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝒫 𝐴
× 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) |
50 | | endomtr 7900 |
. . . . . . . 8
⊢
((𝒫 (𝒫 𝐴 +𝑐 (har‘𝐴)) ≈ (𝒫 𝒫
𝐴 × 𝒫
(har‘𝐴)) ∧
(𝒫 𝒫 𝐴
× 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) → 𝒫 (𝒫
𝐴 +𝑐
(har‘𝐴)) ≼
𝒫 𝒫 𝐴) |
51 | 16, 49, 50 | syl2anc 691 |
. . . . . . 7
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝒫 𝐴
+𝑐 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) |
52 | | sdomdomtr 7978 |
. . . . . . 7
⊢
(((𝒫 𝐴
+𝑐 (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 +𝑐
(har‘𝐴)) ∧
𝒫 (𝒫 𝐴
+𝑐 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) → (𝒫 𝐴 +𝑐
(har‘𝐴)) ≺
𝒫 𝒫 𝐴) |
53 | 14, 51, 52 | sylancr 694 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝐴
+𝑐 (har‘𝐴)) ≺ 𝒫 𝒫 𝐴) |
54 | | gchen1 9326 |
. . . . . 6
⊢
(((𝒫 𝐴
∈ GCH ∧ ¬ 𝒫 𝐴 ∈ Fin) ∧ (𝒫 𝐴 ≼ (𝒫 𝐴 +𝑐
(har‘𝐴)) ∧
(𝒫 𝐴
+𝑐 (har‘𝐴)) ≺ 𝒫 𝒫 𝐴)) → 𝒫 𝐴 ≈ (𝒫 𝐴 +𝑐
(har‘𝐴))) |
55 | 2, 10, 12, 53, 54 | syl22anc 1319 |
. . . . 5
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ≈
(𝒫 𝐴
+𝑐 (har‘𝐴))) |
56 | | cdacomen 8886 |
. . . . 5
⊢
(𝒫 𝐴
+𝑐 (har‘𝐴)) ≈ ((har‘𝐴) +𝑐 𝒫 𝐴) |
57 | | entr 7894 |
. . . . 5
⊢
((𝒫 𝐴
≈ (𝒫 𝐴
+𝑐 (har‘𝐴)) ∧ (𝒫 𝐴 +𝑐 (har‘𝐴)) ≈ ((har‘𝐴) +𝑐
𝒫 𝐴)) →
𝒫 𝐴 ≈
((har‘𝐴)
+𝑐 𝒫 𝐴)) |
58 | 55, 56, 57 | sylancl 693 |
. . . 4
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ≈
((har‘𝐴)
+𝑐 𝒫 𝐴)) |
59 | 58 | ensymd 7893 |
. . 3
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
((har‘𝐴)
+𝑐 𝒫 𝐴) ≈ 𝒫 𝐴) |
60 | | domentr 7901 |
. . 3
⊢
(((har‘𝐴)
≼ ((har‘𝐴)
+𝑐 𝒫 𝐴) ∧ ((har‘𝐴) +𝑐 𝒫 𝐴) ≈ 𝒫 𝐴) → (har‘𝐴) ≼ 𝒫 𝐴) |
61 | 4, 59, 60 | syl2anc 691 |
. 2
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(har‘𝐴) ≼
𝒫 𝐴) |
62 | | gchcdaidm 9369 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐 𝐴) ≈ 𝐴) |
63 | 19, 8, 62 | syl2anc 691 |
. . . . 5
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 +𝑐 𝐴) ≈ 𝐴) |
64 | | pwen 8018 |
. . . . 5
⊢ ((𝐴 +𝑐 𝐴) ≈ 𝐴 → 𝒫 (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴) |
65 | 63, 64 | syl 17 |
. . . 4
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝐴
+𝑐 𝐴)
≈ 𝒫 𝐴) |
66 | | cdadom3 8893 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧
(har‘𝐴) ∈ On)
→ 𝐴 ≼ (𝐴 +𝑐
(har‘𝐴))) |
67 | 19, 1, 66 | sylancl 693 |
. . . . . . 7
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → 𝐴 ≼ (𝐴 +𝑐 (har‘𝐴))) |
68 | | harndom 8352 |
. . . . . . . 8
⊢ ¬
(har‘𝐴) ≼ 𝐴 |
69 | | cdadom3 8893 |
. . . . . . . . . . 11
⊢
(((har‘𝐴)
∈ On ∧ 𝐴 ∈
GCH) → (har‘𝐴)
≼ ((har‘𝐴)
+𝑐 𝐴)) |
70 | 1, 19, 69 | sylancr 694 |
. . . . . . . . . 10
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(har‘𝐴) ≼
((har‘𝐴)
+𝑐 𝐴)) |
71 | | cdacomen 8886 |
. . . . . . . . . 10
⊢
((har‘𝐴)
+𝑐 𝐴)
≈ (𝐴
+𝑐 (har‘𝐴)) |
72 | | domentr 7901 |
. . . . . . . . . 10
⊢
(((har‘𝐴)
≼ ((har‘𝐴)
+𝑐 𝐴)
∧ ((har‘𝐴)
+𝑐 𝐴)
≈ (𝐴
+𝑐 (har‘𝐴))) → (har‘𝐴) ≼ (𝐴 +𝑐 (har‘𝐴))) |
73 | 70, 71, 72 | sylancl 693 |
. . . . . . . . 9
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(har‘𝐴) ≼
(𝐴 +𝑐
(har‘𝐴))) |
74 | | domen2 7988 |
. . . . . . . . 9
⊢ (𝐴 ≈ (𝐴 +𝑐 (har‘𝐴)) → ((har‘𝐴) ≼ 𝐴 ↔ (har‘𝐴) ≼ (𝐴 +𝑐 (har‘𝐴)))) |
75 | 73, 74 | syl5ibrcom 236 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 ≈ (𝐴 +𝑐 (har‘𝐴)) → (har‘𝐴) ≼ 𝐴)) |
76 | 68, 75 | mtoi 189 |
. . . . . . 7
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → ¬
𝐴 ≈ (𝐴 +𝑐
(har‘𝐴))) |
77 | | brsdom 7864 |
. . . . . . 7
⊢ (𝐴 ≺ (𝐴 +𝑐 (har‘𝐴)) ↔ (𝐴 ≼ (𝐴 +𝑐 (har‘𝐴)) ∧ ¬ 𝐴 ≈ (𝐴 +𝑐 (har‘𝐴)))) |
78 | 67, 76, 77 | sylanbrc 695 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → 𝐴 ≺ (𝐴 +𝑐 (har‘𝐴))) |
79 | | canth2g 7999 |
. . . . . . . . 9
⊢ (𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴) |
80 | | sdomdom 7869 |
. . . . . . . . 9
⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴) |
81 | | cdadom1 8891 |
. . . . . . . . 9
⊢ (𝐴 ≼ 𝒫 𝐴 → (𝐴 +𝑐 (har‘𝐴)) ≼ (𝒫 𝐴 +𝑐
(har‘𝐴))) |
82 | 19, 79, 80, 81 | 4syl 19 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 +𝑐
(har‘𝐴)) ≼
(𝒫 𝐴
+𝑐 (har‘𝐴))) |
83 | | cdadom2 8892 |
. . . . . . . . 9
⊢
((har‘𝐴)
≼ 𝒫 𝐴 →
(𝒫 𝐴
+𝑐 (har‘𝐴)) ≼ (𝒫 𝐴 +𝑐 𝒫 𝐴)) |
84 | 61, 83 | syl 17 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝐴
+𝑐 (har‘𝐴)) ≼ (𝒫 𝐴 +𝑐 𝒫 𝐴)) |
85 | | domtr 7895 |
. . . . . . . 8
⊢ (((𝐴 +𝑐
(har‘𝐴)) ≼
(𝒫 𝐴
+𝑐 (har‘𝐴)) ∧ (𝒫 𝐴 +𝑐 (har‘𝐴)) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴)) → (𝐴 +𝑐
(har‘𝐴)) ≼
(𝒫 𝐴
+𝑐 𝒫 𝐴)) |
86 | 82, 84, 85 | syl2anc 691 |
. . . . . . 7
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 +𝑐
(har‘𝐴)) ≼
(𝒫 𝐴
+𝑐 𝒫 𝐴)) |
87 | | domentr 7901 |
. . . . . . 7
⊢ (((𝐴 +𝑐
(har‘𝐴)) ≼
(𝒫 𝐴
+𝑐 𝒫 𝐴) ∧ (𝒫 𝐴 +𝑐 𝒫 𝐴) ≈ 𝒫 𝐴) → (𝐴 +𝑐 (har‘𝐴)) ≼ 𝒫 𝐴) |
88 | 86, 41, 87 | syl2anc 691 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 +𝑐
(har‘𝐴)) ≼
𝒫 𝐴) |
89 | | gchen2 9327 |
. . . . . 6
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≺ (𝐴 +𝑐 (har‘𝐴)) ∧ (𝐴 +𝑐 (har‘𝐴)) ≼ 𝒫 𝐴)) → (𝐴 +𝑐 (har‘𝐴)) ≈ 𝒫 𝐴) |
90 | 19, 8, 78, 88, 89 | syl22anc 1319 |
. . . . 5
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 +𝑐
(har‘𝐴)) ≈
𝒫 𝐴) |
91 | 90 | ensymd 7893 |
. . . 4
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ≈ (𝐴 +𝑐
(har‘𝐴))) |
92 | | entr 7894 |
. . . 4
⊢
((𝒫 (𝐴
+𝑐 𝐴)
≈ 𝒫 𝐴 ∧
𝒫 𝐴 ≈ (𝐴 +𝑐
(har‘𝐴))) →
𝒫 (𝐴
+𝑐 𝐴)
≈ (𝐴
+𝑐 (har‘𝐴))) |
93 | 65, 91, 92 | syl2anc 691 |
. . 3
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝐴
+𝑐 𝐴)
≈ (𝐴
+𝑐 (har‘𝐴))) |
94 | | endom 7868 |
. . 3
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≈ (𝐴
+𝑐 (har‘𝐴)) → 𝒫 (𝐴 +𝑐 𝐴) ≼ (𝐴 +𝑐 (har‘𝐴))) |
95 | | pwcdadom 8921 |
. . 3
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 (har‘𝐴)) → 𝒫 𝐴 ≼ (har‘𝐴)) |
96 | 93, 94, 95 | 3syl 18 |
. 2
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ≼
(har‘𝐴)) |
97 | | sbth 7965 |
. 2
⊢
(((har‘𝐴)
≼ 𝒫 𝐴 ∧
𝒫 𝐴 ≼
(har‘𝐴)) →
(har‘𝐴) ≈
𝒫 𝐴) |
98 | 61, 96, 97 | syl2anc 691 |
1
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(har‘𝐴) ≈
𝒫 𝐴) |