This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐴 ) ≈ 𝒫 𝐴 → 𝐴 ∈ GCH )

Proof

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