This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY The Generalized Continuum Hypothesis Derivation of the Axiom of Choice 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 ⊢ ( ( ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH ) → 𝒫 𝐴 ∈ dom card )
Proof
Step
Hyp
Ref
Expression
1
harcl ⊢ ( har ‘ 𝐴 ) ∈ On
2
gchhar ⊢ ( ( ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH ) → ( har ‘ 𝐴 ) ≈ 𝒫 𝐴 )
3
isnumi ⊢ ( ( ( har ‘ 𝐴 ) ∈ On ∧ ( har ‘ 𝐴 ) ≈ 𝒫 𝐴 ) → 𝒫 𝐴 ∈ dom card )
4
1 2 3
sylancr ⊢ ( ( ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH ) → 𝒫 𝐴 ∈ dom card )