MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  aleph1re Structured version   Visualization version   GIF version

Theorem aleph1re 14457
Description: There are at least aleph-one real numbers. (Contributed by NM, 2-Feb-2005.)
Assertion
Ref Expression
aleph1re (ℵ‘1𝑜) ≼ ℝ

Proof of Theorem aleph1re
StepHypRef Expression
1 aleph0 8582 . . . . . 6 (ℵ‘∅) = ω
2 nnenom 12306 . . . . . . 7 ℕ ≈ ω
32ensymi 7703 . . . . . 6 ω ≈ ℕ
41, 3eqbrtri 4454 . . . . 5 (ℵ‘∅) ≈ ℕ
5 ruc 14455 . . . . 5 ℕ ≺ ℝ
6 ensdomtr 7792 . . . . 5 (((ℵ‘∅) ≈ ℕ ∧ ℕ ≺ ℝ) → (ℵ‘∅) ≺ ℝ)
74, 5, 6mp2an 695 . . . 4 (ℵ‘∅) ≺ ℝ
8 alephnbtwn2 8588 . . . 4 ¬ ((ℵ‘∅) ≺ ℝ ∧ ℝ ≺ (ℵ‘suc ∅))
97, 8mptnan 1681 . . 3 ¬ ℝ ≺ (ℵ‘suc ∅)
10 df-1o 7259 . . . . 5 1𝑜 = suc ∅
1110fveq2i 5930 . . . 4 (ℵ‘1𝑜) = (ℵ‘suc ∅)
1211breq2i 4442 . . 3 (ℝ ≺ (ℵ‘1𝑜) ↔ ℝ ≺ (ℵ‘suc ∅))
139, 12mtbir 308 . 2 ¬ ℝ ≺ (ℵ‘1𝑜)
14 fvex 5937 . . 3 (ℵ‘1𝑜) ∈ V
15 reex 9715 . . 3 ℝ ∈ V
16 domtri 9066 . . 3 (((ℵ‘1𝑜) ∈ V ∧ ℝ ∈ V) → ((ℵ‘1𝑜) ≼ ℝ ↔ ¬ ℝ ≺ (ℵ‘1𝑜)))
1714, 15, 16mp2an 695 . 2 ((ℵ‘1𝑜) ≼ ℝ ↔ ¬ ℝ ≺ (ℵ‘1𝑜))
1813, 17mpbir 216 1 (ℵ‘1𝑜) ≼ ℝ
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 191  wcel 1937  Vcvv 3066  c0 3757   class class class wbr 4434  suc csuc 5476  cfv 5633  ωcom 6769  1𝑜c1o 7252  cen 7649  cdom 7650  csdm 7651  cale 8455  cr 9623  cn 10698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-rep 4548  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680  ax-un 6659  ax-inf2 8231  ax-ac2 8978  ax-cnex 9680  ax-resscn 9681  ax-1cn 9682  ax-icn 9683  ax-addcl 9684  ax-addrcl 9685  ax-mulcl 9686  ax-mulrcl 9687  ax-mulcom 9688  ax-addass 9689  ax-mulass 9690  ax-distr 9691  ax-i2m1 9692  ax-1ne0 9693  ax-1rid 9694  ax-rnegex 9695  ax-rrecex 9696  ax-cnre 9697  ax-pre-lttri 9698  ax-pre-lttrn 9699  ax-pre-ltadd 9700  ax-pre-mulgt0 9701  ax-pre-sup 9702
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-fal 1474  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-nel 2678  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-int 4265  df-iun 4309  df-br 4435  df-opab 4494  df-mpt 4495  df-tr 4531  df-eprel 4791  df-id 4795  df-po 4801  df-so 4802  df-fr 4839  df-se 4840  df-we 4841  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-pred 5431  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-iota 5597  df-fun 5635  df-fn 5636  df-f 5637  df-f1 5638  df-fo 5639  df-f1o 5640  df-fv 5641  df-isom 5642  df-riota 6325  df-ov 6366  df-oprab 6367  df-mpt2 6368  df-om 6770  df-1st 6870  df-2nd 6871  df-wrecs 7105  df-recs 7167  df-rdg 7205  df-1o 7259  df-er 7440  df-en 7653  df-dom 7654  df-sdom 7655  df-fin 7656  df-sup 8041  df-oi 8108  df-har 8156  df-card 8458  df-aleph 8459  df-ac 8632  df-pnf 9762  df-mnf 9763  df-xr 9764  df-ltxr 9765  df-le 9766  df-sub 9949  df-neg 9950  df-div 10359  df-nn 10699  df-2 10757  df-n0 10961  df-z 11029  df-uz 11250  df-fz 11881  df-seq 12328
This theorem is referenced by:  aleph1irr  14458
  Copyright terms: Public domain W3C validator