Theorem ruc 16262

Description: The set of positive integers is strictly dominated by the set of real numbers, i.e. the real numbers are uncountable. The proof consists of lemmas ruclem1 16250 through ruclem13 16261 and this final piece. Our proof is based on the proof of Theorem 5.18 of [Truss] p. 114. See ruclem13 16261 for the function existence version of this theorem. For an informal discussion of this proof, see mmcomplex.html#uncountable 16261. For an alternate proof see rucALT 16249. This is Metamath 100 proof #22. (Contributed by NM, 13-Oct-2004.)

Assertion

Ref	Expression
ruc	⊢ ℕ ≺ ℝ

Proof of Theorem ruc

Step	Hyp	Ref	Expression
1		reex 11230	. . 3 ⊢ ℝ ∈ V
2		nnssre 12254	. . 3 ⊢ ℕ ⊆ ℝ
3		ssdomg 9026	. . 3 ⊢ (ℝ ∈ V → (ℕ ⊆ ℝ → ℕ ≼ ℝ))
4	1, 2, 3	mp2 9	. 2 ⊢ ℕ ≼ ℝ
5		ruclem13 16261	. . . . 5 ⊢ ¬ 𝑓:ℕ–onto→ℝ
6		f1ofo 6844	. . . . 5 ⊢ (𝑓:ℕ–1-1-onto→ℝ → 𝑓:ℕ–onto→ℝ)
7	5, 6	mto 197	. . . 4 ⊢ ¬ 𝑓:ℕ–1-1-onto→ℝ
8	7	nex 1796	. . 3 ⊢ ¬ ∃𝑓 𝑓:ℕ–1-1-onto→ℝ
9		bren 8981	. . 3 ⊢ (ℕ ≈ ℝ ↔ ∃𝑓 𝑓:ℕ–1-1-onto→ℝ)
10	8, 9	mtbir 323	. 2 ⊢ ¬ ℕ ≈ ℝ
11		brsdom 9001	. 2 ⊢ (ℕ ≺ ℝ ↔ (ℕ ≼ ℝ ∧ ¬ ℕ ≈ ℝ))
12	4, 10, 11	mpbir2an 711	1 ⊢ ℕ ≺ ℝ

Syntax hints:  ¬ wn 3  ∃wex 1775   ∈ wcel 2105  Vcvv 3477   ⊆ wss 3962   class class class wbr 5146  –onto→wfo 6550  –1-1-onto→wf1o 6551   ≈ cen 8968   ≼ cdom 8969   ≺ csdm 8970  ℝcr 11138  ℕcn 12250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5283  ax-sep 5297  ax-nul 5304  ax-pow 5363  ax-pr 5427  ax-un 7741  ax-cnex 11195  ax-resscn 11196  ax-1cn 11197  ax-icn 11198  ax-addcl 11199  ax-addrcl 11200  ax-mulcl 11201  ax-mulrcl 11202  ax-mulcom 11203  ax-addass 11204  ax-mulass 11205  ax-distr 11206  ax-i2m1 11207  ax-1ne0 11208  ax-1rid 11209  ax-rnegex 11210  ax-rrecex 11211  ax-cnre 11212  ax-pre-lttri 11213  ax-pre-lttrn 11214  ax-pre-ltadd 11215  ax-pre-mulgt0 11216  ax-pre-sup 11217

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5147  df-opab 5209  df-mpt 5230  df-tr 5264  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5630  df-we 5632  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6312  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6554  df-fn 6555  df-f 6556  df-f1 6557  df-fo 6558  df-f1o 6559  df-fv 6560  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7875  df-1st 8000  df-2nd 8001  df-frecs 8292  df-wrecs 8323  df-recs 8397  df-rdg 8436  df-er 8731  df-en 8972  df-dom 8973  df-sdom 8974  df-sup 9466  df-pnf 11281  df-mnf 11282  df-xr 11283  df-ltxr 11284  df-le 11285  df-sub 11478  df-neg 11479  df-div 11905  df-nn 12251  df-2 12313  df-n0 12511  df-z 12598  df-uz 12863  df-fz 13531  df-seq 14026

This theorem is referenced by:  resdomq  16263  aleph1re  16264  aleph1irr  16265