Theorem axresscn 6216

Description: The real numbers are a subset of the complex numbers. Axiom 2 of 25 for real and complex numbers, derived from ZF set theory. (The proof was shortened by Andrew Salmon, 12-Aug-2011.)

Assertion

Ref	Expression
axresscn	|- RR C_ CC

Proof of Theorem axresscn

Step	Hyp	Ref	Expression
1		0r 6137	. . . 4 |- 0R e. R.
2		snssi 2951	. . . 4 |- (0R e. R. -> {0R} C_ R.)
3	1, 2	ax-mp 7	. . 3 |- {0R} C_ R.
4		xpss2 3903	. . 3 |- ({0R} C_ R. -> (R. X. {0R}) C_ (R. X. R.))
5	3, 4	ax-mp 7	. 2 |- (R. X. {0R}) C_ (R. X. R.)
6		df-r 6192	. 2 |- RR = (R. X. {0R})
7		df-c 6188	. 2 |- CC = (R. X. R.)
8	5, 6, 7	3sstr4i 2489	1 |- RR C_ CC

Syntax hints:   e. wcel 1138   C_ wss 2426  {csn 2868   X. cxp 3795  R.cnr 5941  0Rc0r 5942  CCcc 6180  RRcr 6181

This theorem is referenced by:  ax1cn 6218  reex 6261  recn 6262  recni 6263  nnsscn 6906  nn0sscn 7108  qsscn 7240  ser1monoi 7545  reexpcl 7618  rpexpcl 7620  nthruc 7790  seq1ublem 7958  ser1absdiflem 7976  climserzlei 8202  climsupi 8210  caucvglem2 8213  caucvgi 8218  cvgcmp2clem 8237  cvgcmp2clemOLD 8238  cvgcmp3ci 8242  abscncf 8332  recncf 8333  imcncf 8334  ivthlem4 8341  ivthlem6 8343  ivthlem7 8344  ivthlem8 8345  ivthlem9 8346  isupivthi 8347  reeff1 8470  reeff1olem1 8484  reeff1o 8486  remetba 8982  readdsubg 9232  abscncfALT 9478  ipasslem7 9632  pilem1 9815  efifolem1 9871  circgrp 9889  ivthALT 15136  fsumltisumii 15504  fsumleisumii 15507  metdcn 15535  iiuni 15550  dfii3 15552  recms 15692  iccbnd 15708  phtpycom 15732  phtpycolem3 15735  phtpycolem4 15736  reparphtlem2 15746  pcocn 15758  pcohtpylem3 15764  pcopt 15766  pcoass 15767  pcorevlem 15768  pcorev 15769  pi1gp 15777

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-rep 3243  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601  ax-inf2 5540

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-reu 1945  df-rab 1946  df-v 2127  df-sbc 2287  df-csb 2374  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-pss 2440  df-nul 2702  df-if 2807  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-int 3037  df-iun 3079  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-id 3401  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476  df-lim 3477  df-suc 3478  df-om 3761  df-xp 3811  df-rel 3812  df-cnv 3813  df-co 3814  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fun 3819  df-fn 3820  df-f 3821  df-fv 3825  df-opr 4697  df-oprab 4698  df-1st 4831  df-2nd 4832  df-rdg 4951  df-1o 4988  df-oadd 4990  df-omul 4991  df-er 5129  df-ec 5131  df-qs 5134  df-ni 5948  df-pli 5949  df-mi 5950  df-lti 5951  df-plpq 5983  df-mpq 5984  df-enq 5985  df-nq 5986  df-plq 5987  df-mq 5988  df-rq 5989  df-ltq 5990  df-1q 5991  df-np 6034  df-1p 6035  df-enr 6114  df-nr 6115  df-0r 6119  df-c 6188  df-r 6192

Copyright terms: Public domain