# Metamath Proof Explorer

## Theorem aleph1re

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

Ref Expression
Assertion aleph1re ${⊢}\aleph \left({1}_{𝑜}\right)\preccurlyeq ℝ$

### Proof

Step Hyp Ref Expression
1 aleph0 ${⊢}\aleph \left(\varnothing \right)=\mathrm{\omega }$
2 nnenom ${⊢}ℕ\approx \mathrm{\omega }$
3 2 ensymi ${⊢}\mathrm{\omega }\approx ℕ$
4 1 3 eqbrtri ${⊢}\aleph \left(\varnothing \right)\approx ℕ$
5 ruc ${⊢}ℕ\prec ℝ$
6 ensdomtr ${⊢}\left(\aleph \left(\varnothing \right)\approx ℕ\wedge ℕ\prec ℝ\right)\to \aleph \left(\varnothing \right)\prec ℝ$
7 4 5 6 mp2an ${⊢}\aleph \left(\varnothing \right)\prec ℝ$
8 alephnbtwn2 ${⊢}¬\left(\aleph \left(\varnothing \right)\prec ℝ\wedge ℝ\prec \aleph \left(\mathrm{suc}\varnothing \right)\right)$
9 7 8 mptnan ${⊢}¬ℝ\prec \aleph \left(\mathrm{suc}\varnothing \right)$
10 df-1o ${⊢}{1}_{𝑜}=\mathrm{suc}\varnothing$
11 10 fveq2i ${⊢}\aleph \left({1}_{𝑜}\right)=\aleph \left(\mathrm{suc}\varnothing \right)$
12 11 breq2i ${⊢}ℝ\prec \aleph \left({1}_{𝑜}\right)↔ℝ\prec \aleph \left(\mathrm{suc}\varnothing \right)$
13 9 12 mtbir ${⊢}¬ℝ\prec \aleph \left({1}_{𝑜}\right)$
14 fvex ${⊢}\aleph \left({1}_{𝑜}\right)\in \mathrm{V}$
15 reex ${⊢}ℝ\in \mathrm{V}$
16 domtri ${⊢}\left(\aleph \left({1}_{𝑜}\right)\in \mathrm{V}\wedge ℝ\in \mathrm{V}\right)\to \left(\aleph \left({1}_{𝑜}\right)\preccurlyeq ℝ↔¬ℝ\prec \aleph \left({1}_{𝑜}\right)\right)$
17 14 15 16 mp2an ${⊢}\aleph \left({1}_{𝑜}\right)\preccurlyeq ℝ↔¬ℝ\prec \aleph \left({1}_{𝑜}\right)$
18 13 17 mpbir ${⊢}\aleph \left({1}_{𝑜}\right)\preccurlyeq ℝ$