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

Theorem ressxr 10121
Description: The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
ressxr ℝ ⊆ ℝ*

Proof of Theorem ressxr
StepHypRef Expression
1 ssun1 3809 . 2 ℝ ⊆ (ℝ ∪ {+∞, -∞})
2 df-xr 10116 . 2 * = (ℝ ∪ {+∞, -∞})
31, 2sseqtr4i 3671 1 ℝ ⊆ ℝ*
Colors of variables: wff setvar class
Syntax hints:  cun 3605  wss 3607  {cpr 4212  cr 9973  +∞cpnf 10109  -∞cmnf 10110  *cxr 10111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-in 3614  df-ss 3621  df-xr 10116
This theorem is referenced by:  rexpssxrxp  10122  rexr  10123  0xr  10124  rexrd  10127  ltrelxr  10137  supxrre  12195  supxrbnd  12196  supxrgtmnf  12197  supxrre1  12198  supxrre2  12199  infxrre  12204  iooval2  12246  fzval2  12367  uzsup  12702  hashxrcl  13186  seqcoll  13286  limsupval2  14255  limsupgre  14256  limsupbnd2  14258  rlimuni  14325  rlimcld2  14353  rlimno1  14428  isercolllem2  14440  isercoll  14442  caucvgrlem  14447  summolem2a  14490  prodmolem2a  14708  ramtlecl  15751  ramxrcl  15768  ismet2  22185  prdsmet  22222  qtopbas  22610  tgqioo  22650  re2ndc  22651  xrsmopn  22662  metdcn2  22689  metdscn2  22707  bndth  22804  ovolunlem1a  23310  ovolunlem1  23311  ovoliunlem1  23316  ovoliun  23319  ovolicc2lem4  23334  voliunlem2  23365  voliunlem3  23366  opnmblALT  23417  vitalilem4  23425  mbfimaopnlem  23467  itg2le  23551  itg2seq  23554  dvfsumrlim  23839  itgsubst  23857  mdegleb  23869  mdeglt  23870  mdegldg  23871  mdegxrcl  23872  mdegcl  23874  mdegaddle  23879  mdegmullem  23883  deg1mul3le  23921  ig1pdvds  23981  aannenlem2  24129  taylfval  24158  radcnvcl  24216  radcnvlt1  24217  radcnvle  24219  xrlimcnp  24740  nmoxr  27749  nmooge0  27750  nmoolb  27754  nmoubi  27755  nmlno0lem  27776  nmopxr  28853  nmfnxr  28866  nmoplb  28894  nmopub  28895  nmfnlb  28911  nmfnleub  28912  nmlnop0iALT  28982  nmopun  29001  branmfn  29092  pjnmopi  29135  xlt2addrd  29651  xreceu  29758  rexdiv  29762  xrsmulgzz  29806  esumcst  30253  icorempt2  33329  mblfinlem2  33577  itg2addnc  33594  prdsbnd  33722  rrnequiv  33764  hbtlem2  38011  binomcxplemdvbinom  38869  binomcxplemcvg  38870  binomcxplemnotnn0  38872  suplesup  39868  frexr  39917  zssxr  39934  ssrexr  39972  uzxrd  40005  supminfxr  40007  rpssxr  40024  elicores  40078  ressiocsup  40099  ressioosup  40100  ressiooinf  40102  uzinico  40105  limsupre  40191  limsupresico  40250  limsuppnfdlem  40251  limsupmnflem  40270  limsupvaluz2  40288  supcnvlimsup  40290  liminfresico  40321  volicoff  40530  volicofmpt  40532  fourierdlem52  40693  fourierdlem103  40744  fourierdlem104  40745  etransclem48  40817  ioorrnopnlem  40842  fsumlesge0  40912  sge0cl  40916  sge0supre  40924  sge0less  40927  sge0split  40944  sge0seq  40981  hoicvr  41083  volicorescl  41088  ovolval2lem  41178  ovolval5lem2  41188  ovnovollem1  41191  ovnovollem2  41192  iinhoiicclem  41208  iunhoiioolem  41210  iccvonmbllem  41213  vonioolem2  41216  vonioo  41217  vonicclem2  41219  vonicc  41220  pimdecfgtioc  41246  pimincfltioc  41247  pimdecfgtioo  41248  pimincfltioo  41249  smflimsuplem4  41350
  Copyright terms: Public domain W3C validator