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

Theorem ressxr 10027
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 3754 . 2 ℝ ⊆ (ℝ ∪ {+∞, -∞})
2 df-xr 10022 . 2 * = (ℝ ∪ {+∞, -∞})
31, 2sseqtr4i 3617 1 ℝ ⊆ ℝ*
Colors of variables: wff setvar class
Syntax hints:  cun 3553  wss 3555  {cpr 4150  cr 9879  +∞cpnf 10015  -∞cmnf 10016  *cxr 10017
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3560  df-in 3562  df-ss 3569  df-xr 10022
This theorem is referenced by:  rexpssxrxp  10028  rexr  10029  0xr  10030  rexrd  10033  ltrelxr  10043  supxrre  12100  supxrbnd  12101  supxrgtmnf  12102  supxrre1  12103  supxrre2  12104  infxrre  12109  iooval2  12150  fzval2  12271  uzsup  12602  hashxrcl  13088  seqcoll  13186  limsupval2  14145  limsupgre  14146  limsupbnd2  14148  rlimuni  14215  rlimcld2  14243  rlimno1  14318  isercolllem2  14330  isercoll  14332  caucvgrlem  14337  summolem2a  14379  prodmolem2a  14589  ramtlecl  15628  ramxrcl  15645  ismet2  22048  prdsmet  22085  qtopbas  22473  tgqioo  22511  re2ndc  22512  xrsmopn  22523  metdcn2  22550  metdscn2  22568  bndth  22665  ovolunlem1a  23171  ovolunlem1  23172  ovoliunlem1  23177  ovoliun  23180  ovolicc2lem4  23195  voliunlem2  23226  voliunlem3  23227  opnmblALT  23277  vitalilem4  23286  mbfimaopnlem  23328  itg2le  23412  itg2seq  23415  dvfsumrlim  23698  itgsubst  23716  mdegleb  23728  mdeglt  23729  mdegldg  23730  mdegxrcl  23731  mdegcl  23733  mdegaddle  23738  mdegmullem  23742  deg1mul3le  23780  ig1pdvds  23840  aannenlem2  23988  taylfval  24017  radcnvcl  24075  radcnvlt1  24076  radcnvle  24078  xrlimcnp  24595  nmoxr  27467  nmooge0  27468  nmoolb  27472  nmoubi  27473  nmlno0lem  27494  nmopxr  28571  nmfnxr  28584  nmoplb  28612  nmopub  28613  nmfnlb  28629  nmfnleub  28630  nmlnop0iALT  28700  nmopun  28719  branmfn  28810  pjnmopi  28853  xlt2addrd  29364  xreceu  29412  rexdiv  29416  xrsmulgzz  29460  esumcst  29903  icorempt2  32828  mblfinlem2  33076  itg2addnc  33093  prdsbnd  33221  rrnequiv  33263  hbtlem2  37172  binomcxplemdvbinom  38031  binomcxplemcvg  38032  binomcxplemnotnn0  38034  suplesup  39016  frexr  39065  zssxr  39082  elicores  39168  ressiocsup  39189  ressioosup  39190  ressiooinf  39192  uzinico  39195  limsupre  39274  limsupresico  39333  limsuppnfdlem  39334  limsupmnflem  39353  limsupvaluz2  39371  supcnvlimsup  39373  volicoff  39516  volicofmpt  39518  fourierdlem52  39679  fourierdlem103  39730  fourierdlem104  39731  etransclem48  39803  ioorrnopnlem  39828  fsumlesge0  39898  sge0cl  39902  sge0supre  39910  sge0less  39913  sge0split  39930  sge0seq  39967  hoicvr  40066  volicorescl  40071  ovolval2lem  40161  ovolval5lem2  40171  ovnovollem1  40174  ovnovollem2  40175  iinhoiicclem  40191  iunhoiioolem  40193  iccvonmbllem  40196  vonioolem2  40199  vonioo  40200  vonicclem2  40202  vonicc  40203  pimdecfgtioc  40229  pimincfltioc  40230  pimdecfgtioo  40231  pimincfltioo  40232  smflimsuplem4  40333
  Copyright terms: Public domain W3C validator