| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | harcl 9600 | . . . . . . . . . . . . . 14
⊢
(har‘𝐴) ∈
On | 
| 2 |  | sdomdom 9021 | . . . . . . . . . . . . . 14
⊢ (𝑥 ≺ (har‘𝐴) → 𝑥 ≼ (har‘𝐴)) | 
| 3 |  | ondomen 10078 | . . . . . . . . . . . . . 14
⊢
(((har‘𝐴)
∈ On ∧ 𝑥 ≼
(har‘𝐴)) → 𝑥 ∈ dom
card) | 
| 4 | 1, 2, 3 | sylancr 587 | . . . . . . . . . . . . 13
⊢ (𝑥 ≺ (har‘𝐴) → 𝑥 ∈ dom card) | 
| 5 |  | onenon 9990 | . . . . . . . . . . . . . 14
⊢
((har‘𝐴)
∈ On → (har‘𝐴) ∈ dom card) | 
| 6 | 1, 5 | ax-mp 5 | . . . . . . . . . . . . 13
⊢
(har‘𝐴) ∈
dom card | 
| 7 |  | cardsdom2 10029 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ dom card ∧
(har‘𝐴) ∈ dom
card) → ((card‘𝑥) ∈ (card‘(har‘𝐴)) ↔ 𝑥 ≺ (har‘𝐴))) | 
| 8 | 4, 6, 7 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝑥 ≺ (har‘𝐴) → ((card‘𝑥) ∈
(card‘(har‘𝐴))
↔ 𝑥 ≺
(har‘𝐴))) | 
| 9 | 8 | ibir 268 | . . . . . . . . . . 11
⊢ (𝑥 ≺ (har‘𝐴) → (card‘𝑥) ∈
(card‘(har‘𝐴))) | 
| 10 |  | harcard 10019 | . . . . . . . . . . 11
⊢
(card‘(har‘𝐴)) = (har‘𝐴) | 
| 11 | 9, 10 | eleqtrdi 2850 | . . . . . . . . . 10
⊢ (𝑥 ≺ (har‘𝐴) → (card‘𝑥) ∈ (har‘𝐴)) | 
| 12 |  | elharval 9602 | . . . . . . . . . . 11
⊢
((card‘𝑥)
∈ (har‘𝐴) ↔
((card‘𝑥) ∈ On
∧ (card‘𝑥)
≼ 𝐴)) | 
| 13 | 12 | simprbi 496 | . . . . . . . . . 10
⊢
((card‘𝑥)
∈ (har‘𝐴) →
(card‘𝑥) ≼
𝐴) | 
| 14 | 11, 13 | syl 17 | . . . . . . . . 9
⊢ (𝑥 ≺ (har‘𝐴) → (card‘𝑥) ≼ 𝐴) | 
| 15 |  | cardid2 9994 | . . . . . . . . . 10
⊢ (𝑥 ∈ dom card →
(card‘𝑥) ≈
𝑥) | 
| 16 |  | domen1 9160 | . . . . . . . . . 10
⊢
((card‘𝑥)
≈ 𝑥 →
((card‘𝑥) ≼
𝐴 ↔ 𝑥 ≼ 𝐴)) | 
| 17 | 4, 15, 16 | 3syl 18 | . . . . . . . . 9
⊢ (𝑥 ≺ (har‘𝐴) → ((card‘𝑥) ≼ 𝐴 ↔ 𝑥 ≼ 𝐴)) | 
| 18 | 14, 17 | mpbid 232 | . . . . . . . 8
⊢ (𝑥 ≺ (har‘𝐴) → 𝑥 ≼ 𝐴) | 
| 19 |  | domnsym 9140 | . . . . . . . 8
⊢ (𝑥 ≼ 𝐴 → ¬ 𝐴 ≺ 𝑥) | 
| 20 | 18, 19 | syl 17 | . . . . . . 7
⊢ (𝑥 ≺ (har‘𝐴) → ¬ 𝐴 ≺ 𝑥) | 
| 21 | 20 | con2i 139 | . . . . . 6
⊢ (𝐴 ≺ 𝑥 → ¬ 𝑥 ≺ (har‘𝐴)) | 
| 22 |  | sdomen2 9163 | . . . . . . 7
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
(𝑥 ≺ (har‘𝐴) ↔ 𝑥 ≺ 𝒫 𝐴)) | 
| 23 | 22 | notbid 318 | . . . . . 6
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
(¬ 𝑥 ≺
(har‘𝐴) ↔ ¬
𝑥 ≺ 𝒫 𝐴)) | 
| 24 | 21, 23 | imbitrid 244 | . . . . 5
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
(𝐴 ≺ 𝑥 → ¬ 𝑥 ≺ 𝒫 𝐴)) | 
| 25 |  | imnan 399 | . . . . 5
⊢ ((𝐴 ≺ 𝑥 → ¬ 𝑥 ≺ 𝒫 𝐴) ↔ ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴)) | 
| 26 | 24, 25 | sylib 218 | . . . 4
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴)) | 
| 27 | 26 | alrimiv 1926 | . . 3
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
∀𝑥 ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴)) | 
| 28 | 27 | olcd 874 | . 2
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
(𝐴 ∈ Fin ∨
∀𝑥 ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴))) | 
| 29 |  | relen 8991 | . . . . 5
⊢ Rel
≈ | 
| 30 | 29 | brrelex2i 5741 | . . . 4
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
𝒫 𝐴 ∈
V) | 
| 31 |  | pwexb 7787 | . . . 4
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V) | 
| 32 | 30, 31 | sylibr 234 | . . 3
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
𝐴 ∈
V) | 
| 33 |  | elgch 10663 | . . 3
⊢ (𝐴 ∈ V → (𝐴 ∈ GCH ↔ (𝐴 ∈ Fin ∨ ∀𝑥 ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴)))) | 
| 34 | 32, 33 | syl 17 | . 2
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
(𝐴 ∈ GCH ↔ (𝐴 ∈ Fin ∨ ∀𝑥 ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴)))) | 
| 35 | 28, 34 | mpbird 257 | 1
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
𝐴 ∈
GCH) |