Theorem aleph1irr

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

	Ref	Expression
Assertion	aleph1irr	⊢ ( ℵ ‘ 1o ) ≼ ( ℝ ∖ ℚ )

Proof

Step	Hyp	Ref	Expression
1		aleph1re	⊢ ( ℵ ‘ 1o ) ≼ ℝ
2		reex	⊢ ℝ ∈ V
3		numth3	⊢ ( ℝ ∈ V → ℝ ∈ dom card )
4	2 3	ax-mp	⊢ ℝ ∈ dom card
5		nnenom	⊢ ℕ ≈ ω
6	5	ensymi	⊢ ω ≈ ℕ
7		ruc	⊢ ℕ ≺ ℝ
8		ensdomtr	⊢ ( ( ω ≈ ℕ ∧ ℕ ≺ ℝ ) → ω ≺ ℝ )
9	6 7 8	mp2an	⊢ ω ≺ ℝ
10		sdomdom	⊢ ( ω ≺ ℝ → ω ≼ ℝ )
11	9 10	ax-mp	⊢ ω ≼ ℝ
12		resdomq	⊢ ℚ ≺ ℝ
13		infdif	⊢ ( ( ℝ ∈ dom card ∧ ω ≼ ℝ ∧ ℚ ≺ ℝ ) → ( ℝ ∖ ℚ ) ≈ ℝ )
14	4 11 12 13	mp3an	⊢ ( ℝ ∖ ℚ ) ≈ ℝ
15	14	ensymi	⊢ ℝ ≈ ( ℝ ∖ ℚ )
16		domentr	⊢ ( ( ( ℵ ‘ 1o ) ≼ ℝ ∧ ℝ ≈ ( ℝ ∖ ℚ ) ) → ( ℵ ‘ 1o ) ≼ ( ℝ ∖ ℚ ) )
17	1 15 16	mp2an	⊢ ( ℵ ‘ 1o ) ≼ ( ℝ ∖ ℚ )