Step | Hyp | Ref
| Expression |
1 | | harcl 9019 |
. . . . . . . . . . . . . 14
⊢
(har‘𝐴) ∈
On |
2 | | sdomdom 8531 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ≺ (har‘𝐴) → 𝑥 ≼ (har‘𝐴)) |
3 | | ondomen 9457 |
. . . . . . . . . . . . . 14
⊢
(((har‘𝐴)
∈ On ∧ 𝑥 ≼
(har‘𝐴)) → 𝑥 ∈ dom
card) |
4 | 1, 2, 3 | sylancr 589 |
. . . . . . . . . . . . 13
⊢ (𝑥 ≺ (har‘𝐴) → 𝑥 ∈ dom card) |
5 | | onenon 9372 |
. . . . . . . . . . . . . 14
⊢
((har‘𝐴)
∈ On → (har‘𝐴) ∈ dom card) |
6 | 1, 5 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(har‘𝐴) ∈
dom card |
7 | | cardsdom2 9411 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ dom card ∧
(har‘𝐴) ∈ dom
card) → ((card‘𝑥) ∈ (card‘(har‘𝐴)) ↔ 𝑥 ≺ (har‘𝐴))) |
8 | 4, 6, 7 | sylancl 588 |
. . . . . . . . . . . 12
⊢ (𝑥 ≺ (har‘𝐴) → ((card‘𝑥) ∈
(card‘(har‘𝐴))
↔ 𝑥 ≺
(har‘𝐴))) |
9 | 8 | ibir 270 |
. . . . . . . . . . 11
⊢ (𝑥 ≺ (har‘𝐴) → (card‘𝑥) ∈
(card‘(har‘𝐴))) |
10 | | harcard 9401 |
. . . . . . . . . . 11
⊢
(card‘(har‘𝐴)) = (har‘𝐴) |
11 | 9, 10 | eleqtrdi 2923 |
. . . . . . . . . 10
⊢ (𝑥 ≺ (har‘𝐴) → (card‘𝑥) ∈ (har‘𝐴)) |
12 | | elharval 9021 |
. . . . . . . . . . 11
⊢
((card‘𝑥)
∈ (har‘𝐴) ↔
((card‘𝑥) ∈ On
∧ (card‘𝑥)
≼ 𝐴)) |
13 | 12 | simprbi 499 |
. . . . . . . . . 10
⊢
((card‘𝑥)
∈ (har‘𝐴) →
(card‘𝑥) ≼
𝐴) |
14 | 11, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ≺ (har‘𝐴) → (card‘𝑥) ≼ 𝐴) |
15 | | cardid2 9376 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom card →
(card‘𝑥) ≈
𝑥) |
16 | | domen1 8653 |
. . . . . . . . . 10
⊢
((card‘𝑥)
≈ 𝑥 →
((card‘𝑥) ≼
𝐴 ↔ 𝑥 ≼ 𝐴)) |
17 | 4, 15, 16 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑥 ≺ (har‘𝐴) → ((card‘𝑥) ≼ 𝐴 ↔ 𝑥 ≼ 𝐴)) |
18 | 14, 17 | mpbid 234 |
. . . . . . . 8
⊢ (𝑥 ≺ (har‘𝐴) → 𝑥 ≼ 𝐴) |
19 | | domnsym 8637 |
. . . . . . . 8
⊢ (𝑥 ≼ 𝐴 → ¬ 𝐴 ≺ 𝑥) |
20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ (𝑥 ≺ (har‘𝐴) → ¬ 𝐴 ≺ 𝑥) |
21 | 20 | con2i 141 |
. . . . . 6
⊢ (𝐴 ≺ 𝑥 → ¬ 𝑥 ≺ (har‘𝐴)) |
22 | | sdomen2 8656 |
. . . . . . 7
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
(𝑥 ≺ (har‘𝐴) ↔ 𝑥 ≺ 𝒫 𝐴)) |
23 | 22 | notbid 320 |
. . . . . 6
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
(¬ 𝑥 ≺
(har‘𝐴) ↔ ¬
𝑥 ≺ 𝒫 𝐴)) |
24 | 21, 23 | syl5ib 246 |
. . . . 5
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
(𝐴 ≺ 𝑥 → ¬ 𝑥 ≺ 𝒫 𝐴)) |
25 | | imnan 402 |
. . . . 5
⊢ ((𝐴 ≺ 𝑥 → ¬ 𝑥 ≺ 𝒫 𝐴) ↔ ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴)) |
26 | 24, 25 | sylib 220 |
. . . 4
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴)) |
27 | 26 | alrimiv 1924 |
. . 3
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
∀𝑥 ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴)) |
28 | 27 | olcd 870 |
. 2
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
(𝐴 ∈ Fin ∨
∀𝑥 ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴))) |
29 | | relen 8508 |
. . . . 5
⊢ Rel
≈ |
30 | 29 | brrelex2i 5604 |
. . . 4
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
𝒫 𝐴 ∈
V) |
31 | | pwexb 7482 |
. . . 4
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V) |
32 | 30, 31 | sylibr 236 |
. . 3
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
𝐴 ∈
V) |
33 | | elgch 10038 |
. . 3
⊢ (𝐴 ∈ V → (𝐴 ∈ GCH ↔ (𝐴 ∈ Fin ∨ ∀𝑥 ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴)))) |
34 | 32, 33 | syl 17 |
. 2
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
(𝐴 ∈ GCH ↔ (𝐴 ∈ Fin ∨ ∀𝑥 ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴)))) |
35 | 28, 34 | mpbird 259 |
1
⊢
((har‘𝐴)
≈ 𝒫 𝐴 →
𝐴 ∈
GCH) |