Metamath Proof Explorer

Theorem gchacg

Description: A "local" form of gchac . If A and ~P A are GCH-sets, then ~P A is well-orderable. The proof is due to Specker. Theorem 2.1 of KanamoriPincus p. 419. (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	gchacg	$⊢ (ω ≼ A \land A \in GCH \land 𝒫 A \in GCH) \to 𝒫 A \in dom card$

Proof

Step	Hyp	Ref	Expression
1		harcl	$⊢ har (A) \in On$
2		gchhar	$⊢ (ω ≼ A \land A \in GCH \land 𝒫 A \in GCH) \to har (A) \approx 𝒫 A$
3		isnumi	$⊢ (har (A) \in On \land har (A) \approx 𝒫 A) \to 𝒫 A \in dom card$
4	1 2 3	sylancr	$⊢ (ω ≼ A \land A \in GCH \land 𝒫 A \in GCH) \to 𝒫 A \in dom card$