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 ) ≼ ℝ