Metamath Proof Explorer


Theorem aleph1irr

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

Ref Expression
Assertion aleph1irr 1𝑜

Proof

Step Hyp Ref Expression
1 aleph1re 1𝑜
2 reex V
3 numth3 Vdomcard
4 2 3 ax-mp domcard
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 domcardω
14 4 11 12 13 mp3an
15 14 ensymi
16 domentr 1𝑜1𝑜
17 1 15 16 mp2an 1𝑜