Theorem ruc 7582

Description: The set of natural numbers is strictly dominated by the set of real numbers, i.e. the real numbers are uncountable. The proof consists of lemmas ruclem1 7543 through ruclem39 7581 and this final piece. Our proof is based on the proof of Theorem 5.18 of [Truss] p. 114. See ruclem39 7581 for the function existence version of this theorem. For an informal discussion of this proof, see http://us.metamath.org/mpegif/mmcomplex.html#uncountable.

Assertion

Ref	Expression
ruc	|- NN ~< RR

Proof of Theorem ruc

Step	Hyp	Ref	Expression
1		brsdom 4399	. 2 |- (NN ~< RR <-> (NN ~<_ RR /\ -. NN ~~ RR))
2		reex 5332	. . 3 |- RR e. V
3		nnssre 5941	. . 3 |- NN (_ RR
4		ssdom2g 4427	. . 3 |- (RR e. V -> (NN (_ RR -> NN ~<_ RR))
5	2, 3, 4	mp2 43	. 2 |- NN ~<_ RR
6		ruclem39 7581	. . . . 5 |- -. f:NN-onto->RR
7		f1ofo 3711	. . . . 5 |- (f:NN-1-1-onto->RR -> f:NN-onto->RR)
8	6, 7	mto 106	. . . 4 |- -. f:NN-1-1-onto->RR
9	8	nex 1105	. . 3 |- -. E.f f:NN-1-1-onto->RR
10	2	bren 4395	. . 3 |- (NN ~~ RR <-> E.f f:NN-1-1-onto->RR)
11	9, 10	mtbir 192	. 2 |- -. NN ~~ RR
12	1, 5, 11	mpbir2an 734	1 |- NN ~< RR

Syntax hints:  -. wn 2   e. wcel 962  E.wex 984  Vcvv 1818   (_ wss 2058   class class class wbr 2634  -onto->wfo 3196  -1-1-onto->wf1o 3197   ~~ cen 4382   ~<_ cdom 4383   ~< csdm 4384  RRcr 5253  NNcn 5316

This theorem is referenced by:  resdomq 7583  aleph1re 7584  aleph1irr 7611

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-rep 2708  ax-sep 2718  ax-nul 2725  ax-pow 2758  ax-pr 2795  ax-un 2882  ax-inf2 4642

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 780  df-3an 781  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-nel 1595  df-ral 1656  df-rex 1657  df-reu 1658  df-rab 1659  df-v 1819  df-sbc 1949  df-csb 2012  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-pss 2066  df-nul 2292  df-if 2374  df-pw 2414  df-sn 2424  df-pr 2425  df-tp 2427  df-op 2428  df-uni 2518  df-int 2548  df-iun 2582  df-br 2635  df-opab 2682  df-tr 2696  df-eprel 2848  df-id 2851  df-po 2856  df-so 2866  df-fr 2933  df-we 2950  df-ord 2967  df-on 2968  df-lim 2969  df-suc 2970  df-om 3148  df-xp 3200  df-rel 3201  df-cnv 3202  df-co 3203  df-dm 3204  df-rn 3205  df-res 3206  df-ima 3207  df-fun 3208  df-fn 3209  df-f 3210  df-f1 3211  df-fo 3212  df-f1o 3213  df-fv 3214  df-rdg 3948  df-opr 3981  df-oprab 3982  df-1st 4095  df-2nd 4096  df-1o 4149  df-oadd 4151  df-omul 4152  df-er 4277  df-ec 4279  df-qs 4282  df-en 4386  df-dom 4387  df-sdom 4388  df-sup 4589  df-ni 5020  df-pli 5021  df-mi 5022  df-lti 5023  df-plpq 5055  df-mpq 5056  df-enq 5057  df-nq 5058  df-plq 5059  df-mq 5060  df-rq 5061  df-ltq 5062  df-1q 5063  df-np 5106  df-1p 5107  df-plp 5108  df-mp 5109  df-ltp 5110  df-plpr 5184  df-mpr 5185  df-enr 5186  df-nr 5187  df-plr 5188  df-mr 5189  df-ltr 5190  df-0r 5191  df-1r 5192  df-m1r 5193  df-c 5260  df-0 5261  df-1 5262  df-i 5263  df-r 5264  df-plus 5265  df-mul 5266  df-lt 5267  df-sub 5376  df-neg 5378  df-pnf 5507  df-mnf 5508  df-xr 5509  df-ltxr 5510  df-le 5511  df-div 5723  df-n 5939  df-2 5984  df-3 5985  df-n0 6132  df-z 6168  df-seq1 6509

Copyright terms: Public domain