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 imbitrid ⊢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