![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > aleph1re | Structured version Visualization version GIF version |
Description: There are at least aleph-one real numbers. (Contributed by NM, 2-Feb-2005.) |
Ref | Expression |
---|---|
aleph1re | ⊢ (ℵ‘1𝑜) ≼ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aleph0 9071 | . . . . . 6 ⊢ (ℵ‘∅) = ω | |
2 | nnenom 12965 | . . . . . . 7 ⊢ ℕ ≈ ω | |
3 | 2 | ensymi 8163 | . . . . . 6 ⊢ ω ≈ ℕ |
4 | 1, 3 | eqbrtri 4817 | . . . . 5 ⊢ (ℵ‘∅) ≈ ℕ |
5 | ruc 15163 | . . . . 5 ⊢ ℕ ≺ ℝ | |
6 | ensdomtr 8253 | . . . . 5 ⊢ (((ℵ‘∅) ≈ ℕ ∧ ℕ ≺ ℝ) → (ℵ‘∅) ≺ ℝ) | |
7 | 4, 5, 6 | mp2an 710 | . . . 4 ⊢ (ℵ‘∅) ≺ ℝ |
8 | alephnbtwn2 9077 | . . . 4 ⊢ ¬ ((ℵ‘∅) ≺ ℝ ∧ ℝ ≺ (ℵ‘suc ∅)) | |
9 | 7, 8 | mptnan 1834 | . . 3 ⊢ ¬ ℝ ≺ (ℵ‘suc ∅) |
10 | df-1o 7721 | . . . . 5 ⊢ 1𝑜 = suc ∅ | |
11 | 10 | fveq2i 6347 | . . . 4 ⊢ (ℵ‘1𝑜) = (ℵ‘suc ∅) |
12 | 11 | breq2i 4804 | . . 3 ⊢ (ℝ ≺ (ℵ‘1𝑜) ↔ ℝ ≺ (ℵ‘suc ∅)) |
13 | 9, 12 | mtbir 312 | . 2 ⊢ ¬ ℝ ≺ (ℵ‘1𝑜) |
14 | fvex 6354 | . . 3 ⊢ (ℵ‘1𝑜) ∈ V | |
15 | reex 10211 | . . 3 ⊢ ℝ ∈ V | |
16 | domtri 9562 | . . 3 ⊢ (((ℵ‘1𝑜) ∈ V ∧ ℝ ∈ V) → ((ℵ‘1𝑜) ≼ ℝ ↔ ¬ ℝ ≺ (ℵ‘1𝑜))) | |
17 | 14, 15, 16 | mp2an 710 | . 2 ⊢ ((ℵ‘1𝑜) ≼ ℝ ↔ ¬ ℝ ≺ (ℵ‘1𝑜)) |
18 | 13, 17 | mpbir 221 | 1 ⊢ (ℵ‘1𝑜) ≼ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∈ wcel 2131 Vcvv 3332 ∅c0 4050 class class class wbr 4796 suc csuc 5878 ‘cfv 6041 ωcom 7222 1𝑜c1o 7714 ≈ cen 8110 ≼ cdom 8111 ≺ csdm 8112 ℵcale 8944 ℝcr 10119 ℕcn 11204 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-rep 4915 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 ax-un 7106 ax-inf2 8703 ax-ac2 9469 ax-cnex 10176 ax-resscn 10177 ax-1cn 10178 ax-icn 10179 ax-addcl 10180 ax-addrcl 10181 ax-mulcl 10182 ax-mulrcl 10183 ax-mulcom 10184 ax-addass 10185 ax-mulass 10186 ax-distr 10187 ax-i2m1 10188 ax-1ne0 10189 ax-1rid 10190 ax-rnegex 10191 ax-rrecex 10192 ax-cnre 10193 ax-pre-lttri 10194 ax-pre-lttrn 10195 ax-pre-ltadd 10196 ax-pre-mulgt0 10197 ax-pre-sup 10198 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1627 df-fal 1630 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-nel 3028 df-ral 3047 df-rex 3048 df-reu 3049 df-rmo 3050 df-rab 3051 df-v 3334 df-sbc 3569 df-csb 3667 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-pss 3723 df-nul 4051 df-if 4223 df-pw 4296 df-sn 4314 df-pr 4316 df-tp 4318 df-op 4320 df-uni 4581 df-int 4620 df-iun 4666 df-br 4797 df-opab 4857 df-mpt 4874 df-tr 4897 df-id 5166 df-eprel 5171 df-po 5179 df-so 5180 df-fr 5217 df-se 5218 df-we 5219 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-rn 5269 df-res 5270 df-ima 5271 df-pred 5833 df-ord 5879 df-on 5880 df-lim 5881 df-suc 5882 df-iota 6004 df-fun 6043 df-fn 6044 df-f 6045 df-f1 6046 df-fo 6047 df-f1o 6048 df-fv 6049 df-isom 6050 df-riota 6766 df-ov 6808 df-oprab 6809 df-mpt2 6810 df-om 7223 df-1st 7325 df-2nd 7326 df-wrecs 7568 df-recs 7629 df-rdg 7667 df-1o 7721 df-er 7903 df-en 8114 df-dom 8115 df-sdom 8116 df-fin 8117 df-sup 8505 df-oi 8572 df-har 8620 df-card 8947 df-aleph 8948 df-ac 9121 df-pnf 10260 df-mnf 10261 df-xr 10262 df-ltxr 10263 df-le 10264 df-sub 10452 df-neg 10453 df-div 10869 df-nn 11205 df-2 11263 df-n0 11477 df-z 11562 df-uz 11872 df-fz 12512 df-seq 12988 |
This theorem is referenced by: aleph1irr 15166 |
Copyright terms: Public domain | W3C validator |