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	syl5ib	⊢ ( ( 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 )