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

Metamath Proof Explorer

Theorem alephsucpw

Description: The power set of an aleph dominates the successor aleph. (The Generalized Continuum Hypothesis says they are equinumerous, see gch3 or gchaleph2 .) (Contributed by NM, 27-Aug-2005)

Ref Expression
Assertion alephsucpw ⊢ ℵ ⁡ suc ⁡ A ≼ 𝒫 ℵ ⁡ A

Proof

Step Hyp Ref Expression
1 alephsucpw2 ⊢ ¬ 𝒫 ℵ ⁡ A ≺ ℵ ⁡ suc ⁡ A
2 fvex ⊢ ℵ ⁡ suc ⁡ A ∈ V
3 fvex ⊢ ℵ ⁡ A ∈ V
4 3 pwex ⊢ 𝒫 ℵ ⁡ A ∈ V
5 domtri ⊢ ℵ ⁡ suc ⁡ A ∈ V ∧ 𝒫 ℵ ⁡ A ∈ V → ℵ ⁡ suc ⁡ A ≼ 𝒫 ℵ ⁡ A ↔ ¬ 𝒫 ℵ ⁡ A ≺ ℵ ⁡ suc ⁡ A
6 2 4 5 mp2an ⊢ ℵ ⁡ suc ⁡ A ≼ 𝒫 ℵ ⁡ A ↔ ¬ 𝒫 ℵ ⁡ A ≺ ℵ ⁡ suc ⁡ A
7 1 6 mpbir ⊢ ℵ ⁡ suc ⁡ A ≼ 𝒫 ℵ ⁡ A