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

Metamath Proof Explorer

Theorem aleph1re

Description: There are at least aleph-one real numbers. (Contributed by NM, 2-Feb-2005)

Ref Expression
Assertion aleph1re ⊢ ℵ ⁡ 1 𝑜 ≼ ℝ

Proof

Step Hyp Ref Expression
1 aleph0 ⊢ ℵ ⁡ ∅ = ω
2 nnenom ⊢ ℕ ≈ ω
3 2 ensymi ⊢ ω ≈ ℕ
4 1 3 eqbrtri ⊢ ℵ ⁡ ∅ ≈ ℕ
5 ruc ⊢ ℕ ≺ ℝ
6 ensdomtr ⊢ ℵ ⁡ ∅ ≈ ℕ ∧ ℕ ≺ ℝ → ℵ ⁡ ∅ ≺ ℝ
7 4 5 6 mp2an ⊢ ℵ ⁡ ∅ ≺ ℝ
8 alephnbtwn2 ⊢ ¬ ℵ ⁡ ∅ ≺ ℝ ∧ ℝ ≺ ℵ ⁡ suc ⁡ ∅
9 7 8 mptnan ⊢ ¬ ℝ ≺ ℵ ⁡ suc ⁡ ∅
10 df-1o ⊢ 1 𝑜 = suc ⁡ ∅
11 10 fveq2i ⊢ ℵ ⁡ 1 𝑜 = ℵ ⁡ suc ⁡ ∅
12 11 breq2i ⊢ ℝ ≺ ℵ ⁡ 1 𝑜 ↔ ℝ ≺ ℵ ⁡ suc ⁡ ∅
13 9 12 mtbir ⊢ ¬ ℝ ≺ ℵ ⁡ 1 𝑜
14 fvex ⊢ ℵ ⁡ 1 𝑜 ∈ V
15 reex ⊢ ℝ ∈ V
16 domtri ⊢ ℵ ⁡ 1 𝑜 ∈ V ∧ ℝ ∈ V → ℵ ⁡ 1 𝑜 ≼ ℝ ↔ ¬ ℝ ≺ ℵ ⁡ 1 𝑜
17 14 15 16 mp2an ⊢ ℵ ⁡ 1 𝑜 ≼ ℝ ↔ ¬ ℝ ≺ ℵ ⁡ 1 𝑜
18 13 17 mpbir ⊢ ℵ ⁡ 1 𝑜 ≼ ℝ