Metamath Proof Explorer

Theorem hargch

Description: If A + ~~P A , then A is a GCH-set. The much simpler converse to gchhar . (Contributed by Mario Carneiro, 2-Jun-2015)

Ref Expression
Assertion hargch ⊢ har ⁡ A ≈ 𝒫 A → A ∈ GCH

Proof

Step Hyp Ref Expression
1 harcl ⊢ har ⁡ A ∈ On
2 sdomdom ⊢ x ≺ har ⁡ A → x ≼ har ⁡ A
3 ondomen ⊢ har ⁡ A ∈ On ∧ x ≼ har ⁡ A → x ∈ dom ⁡ card
4 1 2 3 sylancr ⊢ x ≺ har ⁡ A → x ∈ dom ⁡ card
5 onenon ⊢ har ⁡ A ∈ On → har ⁡ A ∈ dom ⁡ card
6 1 5 ax-mp ⊢ har ⁡ A ∈ dom ⁡ card
7 cardsdom2 ⊢ x ∈ dom ⁡ card ∧ har ⁡ A ∈ dom ⁡ card → card ⁡ x ∈ card ⁡ har ⁡ A ↔ x ≺ har ⁡ A
8 4 6 7 sylancl ⊢ x ≺ har ⁡ A → card ⁡ x ∈ card ⁡ har ⁡ A ↔ x ≺ har ⁡ A
9 8 ibir ⊢ x ≺ har ⁡ A → card ⁡ x ∈ card ⁡ har ⁡ A
10 harcard ⊢ card ⁡ har ⁡ A = har ⁡ A
11 9 10 eleqtrdi ⊢ x ≺ har ⁡ A → card ⁡ x ∈ har ⁡ A
12 elharval ⊢ card ⁡ x ∈ har ⁡ A ↔ card ⁡ x ∈ On ∧ card ⁡ x ≼ A
13 12 simprbi ⊢ card ⁡ x ∈ har ⁡ A → card ⁡ x ≼ A
14 11 13 syl ⊢ x ≺ har ⁡ A → card ⁡ x ≼ A
15 cardid2 ⊢ x ∈ dom ⁡ card → card ⁡ x ≈ x
16 domen1 ⊢ card ⁡ x ≈ x → card ⁡ x ≼ A ↔ x ≼ A
17 4 15 16 3syl ⊢ x ≺ har ⁡ A → card ⁡ x ≼ A ↔ x ≼ A
18 14 17 mpbid ⊢ x ≺ har ⁡ A → x ≼ A
19 domnsym ⊢ x ≼ A → ¬ A ≺ x
20 18 19 syl ⊢ x ≺ har ⁡ A → ¬ A ≺ x
21 20 con2i ⊢ A ≺ x → ¬ x ≺ har ⁡ A
22 sdomen2 ⊢ har ⁡ A ≈ 𝒫 A → x ≺ har ⁡ A ↔ x ≺ 𝒫 A
23 22 notbid ⊢ har ⁡ A ≈ 𝒫 A → ¬ x ≺ har ⁡ A ↔ ¬ x ≺ 𝒫 A
24 21 23 syl5ib ⊢ har ⁡ A ≈ 𝒫 A → A ≺ x → ¬ x ≺ 𝒫 A
25 imnan ⊢ A ≺ x → ¬ x ≺ 𝒫 A ↔ ¬ A ≺ x ∧ x ≺ 𝒫 A
26 24 25 sylib ⊢ har ⁡ A ≈ 𝒫 A → ¬ A ≺ x ∧ x ≺ 𝒫 A
27 26 alrimiv ⊢ har ⁡ A ≈ 𝒫 A → ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
28 27 olcd ⊢ har ⁡ A ≈ 𝒫 A → A ∈ Fin ∨ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
29 relen ⊢ Rel ⁡ ≈
30 29 brrelex2i ⊢ har ⁡ A ≈ 𝒫 A → 𝒫 A ∈ V
31 pwexb ⊢ A ∈ V ↔ 𝒫 A ∈ V
32 30 31 sylibr ⊢ har ⁡ A ≈ 𝒫 A → A ∈ V
33 elgch ⊢ A ∈ V → A ∈ GCH ↔ A ∈ Fin ∨ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
34 32 33 syl ⊢ har ⁡ A ≈ 𝒫 A → A ∈ GCH ↔ A ∈ Fin ∨ ∀ x ¬ A ≺ x ∧ x ≺ 𝒫 A
35 28 34 mpbird ⊢ har ⁡ A ≈ 𝒫 A → A ∈ GCH