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 ( ℵ ‘ 1o ) ≼ ℝ

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 ⊢ 1o = suc ∅
11 10 fveq2i ⊢ ( ℵ ‘ 1o ) = ( ℵ ‘ suc ∅ )
12 11 breq2i ⊢ ( ℝ ≺ ( ℵ ‘ 1o ) ↔ ℝ ≺ ( ℵ ‘ suc ∅ ) )
13 9 12 mtbir ⊢ ¬ ℝ ≺ ( ℵ ‘ 1o )
14 fvex ⊢ ( ℵ ‘ 1o ) ∈ V
15 reex ⊢ ℝ ∈ V
16 domtri ⊢ ( ( ( ℵ ‘ 1o ) ∈ V ∧ ℝ ∈ V ) → ( ( ℵ ‘ 1o ) ≼ ℝ ↔ ¬ ℝ ≺ ( ℵ ‘ 1o ) ) )
17 14 15 16 mp2an ⊢ ( ( ℵ ‘ 1o ) ≼ ℝ ↔ ¬ ℝ ≺ ( ℵ ‘ 1o ) )
18 13 17 mpbir ⊢ ( ℵ ‘ 1o ) ≼ ℝ