Metamath Proof Explorer

Theorem aleph1

Description: The set exponentiation of 2 to the aleph-zero has cardinality of at least aleph-one. (If we were to assume the Continuum Hypothesis, their cardinalities would be the same.) (Contributed by NM, 7-Jul-2004)

Ref Expression
Assertion aleph1 ⊢ ℵ ⁡ 1 𝑜 ≼ 2 𝑜 ℵ ⁡ ∅

Proof

Step Hyp Ref Expression
1 df-1o ⊢ 1 𝑜 = suc ⁡ ∅
2 1 fveq2i ⊢ ℵ ⁡ 1 𝑜 = ℵ ⁡ suc ⁡ ∅
3 alephsucpw ⊢ ℵ ⁡ suc ⁡ ∅ ≼ 𝒫 ℵ ⁡ ∅
4 fvex ⊢ ℵ ⁡ ∅ ∈ V
5 4 pw2en ⊢ 𝒫 ℵ ⁡ ∅ ≈ 2 𝑜 ℵ ⁡ ∅
6 domen2 ⊢ 𝒫 ℵ ⁡ ∅ ≈ 2 𝑜 ℵ ⁡ ∅ → ℵ ⁡ suc ⁡ ∅ ≼ 𝒫 ℵ ⁡ ∅ ↔ ℵ ⁡ suc ⁡ ∅ ≼ 2 𝑜 ℵ ⁡ ∅
7 5 6 ax-mp ⊢ ℵ ⁡ suc ⁡ ∅ ≼ 𝒫 ℵ ⁡ ∅ ↔ ℵ ⁡ suc ⁡ ∅ ≼ 2 𝑜 ℵ ⁡ ∅
8 3 7 mpbi ⊢ ℵ ⁡ suc ⁡ ∅ ≼ 2 𝑜 ℵ ⁡ ∅
9 2 8 eqbrtri ⊢ ℵ ⁡ 1 𝑜 ≼ 2 𝑜 ℵ ⁡ ∅