Proof of Theorem gchhar
| Step | Hyp | Ref
| Expression |
| 1 | | harcl 9599 |
. . . 4
⊢
(har‘𝐴) ∈
On |
| 2 | | simp3 1139 |
. . . 4
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ∈
GCH) |
| 3 | | djudoml 10225 |
. . . 4
⊢
(((har‘𝐴)
∈ On ∧ 𝒫 𝐴
∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝒫 𝐴)) |
| 4 | 1, 2, 3 | sylancr 587 |
. . 3
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(har‘𝐴) ≼
((har‘𝐴) ⊔
𝒫 𝐴)) |
| 5 | | domnsym 9139 |
. . . . . . . . 9
⊢ (ω
≼ 𝐴 → ¬
𝐴 ≺
ω) |
| 6 | 5 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → ¬
𝐴 ≺
ω) |
| 7 | | isfinite 9692 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺
ω) |
| 8 | 6, 7 | sylnibr 329 |
. . . . . . 7
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → ¬
𝐴 ∈
Fin) |
| 9 | | pwfi 9357 |
. . . . . . 7
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
| 10 | 8, 9 | sylnib 328 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → ¬
𝒫 𝐴 ∈
Fin) |
| 11 | | djudoml 10225 |
. . . . . . 7
⊢
((𝒫 𝐴 ∈
GCH ∧ (har‘𝐴)
∈ On) → 𝒫 𝐴 ≼ (𝒫 𝐴 ⊔ (har‘𝐴))) |
| 12 | 2, 1, 11 | sylancl 586 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ≼
(𝒫 𝐴 ⊔
(har‘𝐴))) |
| 13 | | fvexd 6921 |
. . . . . . . . 9
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(har‘𝐴) ∈
V) |
| 14 | | djuex 9948 |
. . . . . . . . 9
⊢
((𝒫 𝐴 ∈
GCH ∧ (har‘𝐴)
∈ V) → (𝒫 𝐴 ⊔ (har‘𝐴)) ∈ V) |
| 15 | 2, 13, 14 | syl2anc 584 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝐴 ⊔
(har‘𝐴)) ∈
V) |
| 16 | | canth2g 9171 |
. . . . . . . 8
⊢
((𝒫 𝐴
⊔ (har‘𝐴))
∈ V → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴))) |
| 17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝐴 ⊔
(har‘𝐴)) ≺
𝒫 (𝒫 𝐴
⊔ (har‘𝐴))) |
| 18 | | pwdjuen 10222 |
. . . . . . . . 9
⊢
((𝒫 𝐴 ∈
GCH ∧ (har‘𝐴)
∈ On) → 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫
(har‘𝐴))) |
| 19 | 2, 1, 18 | sylancl 586 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝒫 𝐴
⊔ (har‘𝐴))
≈ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴))) |
| 20 | 2 | pwexd 5379 |
. . . . . . . . . 10
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝒫 𝐴
∈ V) |
| 21 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → 𝐴 ∈ GCH) |
| 22 | | harwdom 9631 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ GCH →
(har‘𝐴)
≼* 𝒫 (𝐴 × 𝐴)) |
| 23 | | wdompwdom 9618 |
. . . . . . . . . . 11
⊢
((har‘𝐴)
≼* 𝒫 (𝐴 × 𝐴) → 𝒫 (har‘𝐴) ≼ 𝒫 𝒫
(𝐴 × 𝐴)) |
| 24 | 21, 22, 23 | 3syl 18 |
. . . . . . . . . 10
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (har‘𝐴)
≼ 𝒫 𝒫 (𝐴 × 𝐴)) |
| 25 | | xpdom2g 9108 |
. . . . . . . . . 10
⊢
((𝒫 𝒫 𝐴 ∈ V ∧ 𝒫 (har‘𝐴) ≼ 𝒫 𝒫
(𝐴 × 𝐴)) → (𝒫 𝒫
𝐴 × 𝒫
(har‘𝐴)) ≼
(𝒫 𝒫 𝐴
× 𝒫 𝒫 (𝐴 × 𝐴))) |
| 26 | 20, 24, 25 | syl2anc 584 |
. . . . . . . . 9
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝒫 𝐴
× 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫
(𝐴 × 𝐴))) |
| 27 | 21, 21 | xpexd 7771 |
. . . . . . . . . . . . 13
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 × 𝐴) ∈ V) |
| 28 | 27 | pwexd 5379 |
. . . . . . . . . . . 12
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝐴 × 𝐴) ∈ V) |
| 29 | | pwdjuen 10222 |
. . . . . . . . . . . 12
⊢
((𝒫 𝐴 ∈
GCH ∧ 𝒫 (𝐴
× 𝐴) ∈ V) →
𝒫 (𝒫 𝐴
⊔ 𝒫 (𝐴
× 𝐴)) ≈
(𝒫 𝒫 𝐴
× 𝒫 𝒫 (𝐴 × 𝐴))) |
| 30 | 2, 28, 29 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝒫 𝐴
⊔ 𝒫 (𝐴
× 𝐴)) ≈
(𝒫 𝒫 𝐴
× 𝒫 𝒫 (𝐴 × 𝐴))) |
| 31 | 30 | ensymd 9045 |
. . . . . . . . . 10
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝒫 𝐴
× 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴))) |
| 32 | | enrefg 9024 |
. . . . . . . . . . . . . 14
⊢
(𝒫 𝐴 ∈
GCH → 𝒫 𝐴
≈ 𝒫 𝐴) |
| 33 | 2, 32 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ≈
𝒫 𝐴) |
| 34 | | gchxpidm 10709 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≈ 𝐴) |
| 35 | 21, 8, 34 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 × 𝐴) ≈ 𝐴) |
| 36 | | pwen 9190 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 × 𝐴) ≈ 𝐴 → 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴) |
| 38 | | djuen 10210 |
. . . . . . . . . . . . 13
⊢
((𝒫 𝐴
≈ 𝒫 𝐴 ∧
𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴) → (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴)) |
| 39 | 33, 37, 38 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝐴 ⊔
𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴)) |
| 40 | | gchdjuidm 10708 |
. . . . . . . . . . . . 13
⊢
((𝒫 𝐴 ∈
GCH ∧ ¬ 𝒫 𝐴
∈ Fin) → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴) |
| 41 | 2, 10, 40 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝐴 ⊔
𝒫 𝐴) ≈
𝒫 𝐴) |
| 42 | | entr 9046 |
. . . . . . . . . . . 12
⊢
(((𝒫 𝐴
⊔ 𝒫 (𝐴
× 𝐴)) ≈
(𝒫 𝐴 ⊔
𝒫 𝐴) ∧
(𝒫 𝐴 ⊔
𝒫 𝐴) ≈
𝒫 𝐴) →
(𝒫 𝐴 ⊔
𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴) |
| 43 | 39, 41, 42 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝐴 ⊔
𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴) |
| 44 | | pwen 9190 |
. . . . . . . . . . 11
⊢
((𝒫 𝐴
⊔ 𝒫 (𝐴
× 𝐴)) ≈
𝒫 𝐴 →
𝒫 (𝒫 𝐴
⊔ 𝒫 (𝐴
× 𝐴)) ≈
𝒫 𝒫 𝐴) |
| 45 | 43, 44 | syl 17 |
. . . . . . . . . 10
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝒫 𝐴
⊔ 𝒫 (𝐴
× 𝐴)) ≈
𝒫 𝒫 𝐴) |
| 46 | | entr 9046 |
. . . . . . . . . 10
⊢
(((𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ∧ 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴) → (𝒫 𝒫
𝐴 × 𝒫
𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫
𝐴) |
| 47 | 31, 45, 46 | syl2anc 584 |
. . . . . . . . 9
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝒫 𝐴
× 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴) |
| 48 | | domentr 9053 |
. . . . . . . . 9
⊢
(((𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫
𝐴 × 𝒫
𝒫 (𝐴 × 𝐴)) ∧ (𝒫 𝒫
𝐴 × 𝒫
𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫
𝐴) → (𝒫
𝒫 𝐴 ×
𝒫 (har‘𝐴))
≼ 𝒫 𝒫 𝐴) |
| 49 | 26, 47, 48 | syl2anc 584 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝒫 𝐴
× 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) |
| 50 | | endomtr 9052 |
. . . . . . . 8
⊢
((𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫
(har‘𝐴)) ∧
(𝒫 𝒫 𝐴
× 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) → 𝒫 (𝒫
𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝒫
𝐴) |
| 51 | 19, 49, 50 | syl2anc 584 |
. . . . . . 7
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝒫 𝐴
⊔ (har‘𝐴))
≼ 𝒫 𝒫 𝐴) |
| 52 | | sdomdomtr 9150 |
. . . . . . 7
⊢
(((𝒫 𝐴
⊔ (har‘𝐴))
≺ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝒫
𝐴) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 𝒫
𝐴) |
| 53 | 17, 51, 52 | syl2anc 584 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝐴 ⊔
(har‘𝐴)) ≺
𝒫 𝒫 𝐴) |
| 54 | | gchen1 10665 |
. . . . . 6
⊢
(((𝒫 𝐴
∈ GCH ∧ ¬ 𝒫 𝐴 ∈ Fin) ∧ (𝒫 𝐴 ≼ (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 𝒫
𝐴)) → 𝒫 𝐴 ≈ (𝒫 𝐴 ⊔ (har‘𝐴))) |
| 55 | 2, 10, 12, 53, 54 | syl22anc 839 |
. . . . 5
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ≈
(𝒫 𝐴 ⊔
(har‘𝐴))) |
| 56 | | djucomen 10218 |
. . . . . 6
⊢
((𝒫 𝐴 ∈
GCH ∧ (har‘𝐴)
∈ V) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ ((har‘𝐴) ⊔ 𝒫 𝐴)) |
| 57 | 2, 13, 56 | syl2anc 584 |
. . . . 5
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝐴 ⊔
(har‘𝐴)) ≈
((har‘𝐴) ⊔
𝒫 𝐴)) |
| 58 | | entr 9046 |
. . . . 5
⊢
((𝒫 𝐴
≈ (𝒫 𝐴
⊔ (har‘𝐴))
∧ (𝒫 𝐴 ⊔
(har‘𝐴)) ≈
((har‘𝐴) ⊔
𝒫 𝐴)) →
𝒫 𝐴 ≈
((har‘𝐴) ⊔
𝒫 𝐴)) |
| 59 | 55, 57, 58 | syl2anc 584 |
. . . 4
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ≈
((har‘𝐴) ⊔
𝒫 𝐴)) |
| 60 | 59 | ensymd 9045 |
. . 3
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
((har‘𝐴) ⊔
𝒫 𝐴) ≈
𝒫 𝐴) |
| 61 | | domentr 9053 |
. . 3
⊢
(((har‘𝐴)
≼ ((har‘𝐴)
⊔ 𝒫 𝐴) ∧
((har‘𝐴) ⊔
𝒫 𝐴) ≈
𝒫 𝐴) →
(har‘𝐴) ≼
𝒫 𝐴) |
| 62 | 4, 60, 61 | syl2anc 584 |
. 2
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(har‘𝐴) ≼
𝒫 𝐴) |
| 63 | | gchdjuidm 10708 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 𝐴) ≈ 𝐴) |
| 64 | 21, 8, 63 | syl2anc 584 |
. . . . 5
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 ⊔ 𝐴) ≈ 𝐴) |
| 65 | | pwen 9190 |
. . . . 5
⊢ ((𝐴 ⊔ 𝐴) ≈ 𝐴 → 𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴) |
| 66 | 64, 65 | syl 17 |
. . . 4
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴) |
| 67 | | djudoml 10225 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧
(har‘𝐴) ∈ On)
→ 𝐴 ≼ (𝐴 ⊔ (har‘𝐴))) |
| 68 | 21, 1, 67 | sylancl 586 |
. . . . . . 7
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → 𝐴 ≼ (𝐴 ⊔ (har‘𝐴))) |
| 69 | | harndom 9602 |
. . . . . . . 8
⊢ ¬
(har‘𝐴) ≼ 𝐴 |
| 70 | | djudoml 10225 |
. . . . . . . . . . 11
⊢
(((har‘𝐴)
∈ On ∧ 𝐴 ∈
GCH) → (har‘𝐴)
≼ ((har‘𝐴)
⊔ 𝐴)) |
| 71 | 1, 21, 70 | sylancr 587 |
. . . . . . . . . 10
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(har‘𝐴) ≼
((har‘𝐴) ⊔
𝐴)) |
| 72 | | djucomen 10218 |
. . . . . . . . . . 11
⊢
(((har‘𝐴)
∈ On ∧ 𝐴 ∈
GCH) → ((har‘𝐴)
⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴))) |
| 73 | 1, 21, 72 | sylancr 587 |
. . . . . . . . . 10
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
((har‘𝐴) ⊔
𝐴) ≈ (𝐴 ⊔ (har‘𝐴))) |
| 74 | | domentr 9053 |
. . . . . . . . . 10
⊢
(((har‘𝐴)
≼ ((har‘𝐴)
⊔ 𝐴) ∧
((har‘𝐴) ⊔
𝐴) ≈ (𝐴 ⊔ (har‘𝐴))) → (har‘𝐴) ≼ (𝐴 ⊔ (har‘𝐴))) |
| 75 | 71, 73, 74 | syl2anc 584 |
. . . . . . . . 9
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(har‘𝐴) ≼
(𝐴 ⊔
(har‘𝐴))) |
| 76 | | domen2 9160 |
. . . . . . . . 9
⊢ (𝐴 ≈ (𝐴 ⊔ (har‘𝐴)) → ((har‘𝐴) ≼ 𝐴 ↔ (har‘𝐴) ≼ (𝐴 ⊔ (har‘𝐴)))) |
| 77 | 75, 76 | syl5ibrcom 247 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 ≈ (𝐴 ⊔ (har‘𝐴)) → (har‘𝐴) ≼ 𝐴)) |
| 78 | 69, 77 | mtoi 199 |
. . . . . . 7
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → ¬
𝐴 ≈ (𝐴 ⊔ (har‘𝐴))) |
| 79 | | brsdom 9015 |
. . . . . . 7
⊢ (𝐴 ≺ (𝐴 ⊔ (har‘𝐴)) ↔ (𝐴 ≼ (𝐴 ⊔ (har‘𝐴)) ∧ ¬ 𝐴 ≈ (𝐴 ⊔ (har‘𝐴)))) |
| 80 | 68, 78, 79 | sylanbrc 583 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → 𝐴 ≺ (𝐴 ⊔ (har‘𝐴))) |
| 81 | | canth2g 9171 |
. . . . . . . . . 10
⊢ (𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴) |
| 82 | | sdomdom 9020 |
. . . . . . . . . 10
⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴) |
| 83 | 21, 81, 82 | 3syl 18 |
. . . . . . . . 9
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → 𝐴 ≼ 𝒫 𝐴) |
| 84 | | djudom1 10223 |
. . . . . . . . 9
⊢ ((𝐴 ≼ 𝒫 𝐴 ∧ (har‘𝐴) ∈ On) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ (har‘𝐴))) |
| 85 | 83, 1, 84 | sylancl 586 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ (har‘𝐴))) |
| 86 | | djudom2 10224 |
. . . . . . . . 9
⊢
(((har‘𝐴)
≼ 𝒫 𝐴 ∧
𝒫 𝐴 ∈ GCH)
→ (𝒫 𝐴
⊔ (har‘𝐴))
≼ (𝒫 𝐴
⊔ 𝒫 𝐴)) |
| 87 | 62, 2, 86 | syl2anc 584 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(𝒫 𝐴 ⊔
(har‘𝐴)) ≼
(𝒫 𝐴 ⊔
𝒫 𝐴)) |
| 88 | | domtr 9047 |
. . . . . . . 8
⊢ (((𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴)) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴)) |
| 89 | 85, 87, 88 | syl2anc 584 |
. . . . . . 7
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴)) |
| 90 | | domentr 9053 |
. . . . . . 7
⊢ (((𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴) ∧ (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴) → (𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝐴) |
| 91 | 89, 41, 90 | syl2anc 584 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝐴) |
| 92 | | gchen2 10666 |
. . . . . 6
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≺ (𝐴 ⊔ (har‘𝐴)) ∧ (𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝐴)) → (𝐴 ⊔ (har‘𝐴)) ≈ 𝒫 𝐴) |
| 93 | 21, 8, 80, 91, 92 | syl22anc 839 |
. . . . 5
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≈ 𝒫 𝐴) |
| 94 | 93 | ensymd 9045 |
. . . 4
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ≈ (𝐴 ⊔ (har‘𝐴))) |
| 95 | | entr 9046 |
. . . 4
⊢
((𝒫 (𝐴
⊔ 𝐴) ≈
𝒫 𝐴 ∧ 𝒫
𝐴 ≈ (𝐴 ⊔ (har‘𝐴))) → 𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴))) |
| 96 | 66, 94, 95 | syl2anc 584 |
. . 3
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴))) |
| 97 | | endom 9019 |
. . 3
⊢
(𝒫 (𝐴
⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)) → 𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ (har‘𝐴))) |
| 98 | | pwdjudom 10255 |
. . 3
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ (har‘𝐴)) → 𝒫 𝐴 ≼ (har‘𝐴)) |
| 99 | 96, 97, 98 | 3syl 18 |
. 2
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
𝒫 𝐴 ≼
(har‘𝐴)) |
| 100 | | sbth 9133 |
. 2
⊢
(((har‘𝐴)
≼ 𝒫 𝐴 ∧
𝒫 𝐴 ≼
(har‘𝐴)) →
(har‘𝐴) ≈
𝒫 𝐴) |
| 101 | 62, 99, 100 | syl2anc 584 |
1
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫
𝐴 ∈ GCH) →
(har‘𝐴) ≈
𝒫 𝐴) |