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

Theorem ressxr 10365
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 3972 . 2 ℝ ⊆ (ℝ ∪ {+∞, -∞})
2 df-xr 10360 . 2 * = (ℝ ∪ {+∞, -∞})
31, 2sseqtr4i 3832 1 ℝ ⊆ ℝ*
Colors of variables: wff setvar class
Syntax hints:  cun 3764  wss 3766  {cpr 4369  cr 10217  +∞cpnf 10353  -∞cmnf 10354  *cxr 10355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-v 3392  df-un 3771  df-in 3773  df-ss 3780  df-xr 10360
This theorem is referenced by:  rexpssxrxp  10366  rexr  10367  0xr  10368  rexrd  10371  ltrelxr  10381  supxrre  12371  supxrbnd  12372  supxrgtmnf  12373  supxrre1  12374  supxrre2  12375  infxrre  12380  iooval2  12422  fzval2  12548  uzsup  12882  hashxrcl  13362  seqcoll  13461  limsupval2  14430  limsupgre  14431  limsupbnd2  14433  rlimuni  14500  rlimcld2  14528  rlimno1  14603  isercolllem2  14615  isercoll  14617  caucvgrlem  14622  summolem2a  14665  prodmolem2a  14881  ramtlecl  15917  ramxrcl  15934  ismet2  22347  prdsmet  22384  qtopbas  22772  tgqioo  22812  re2ndc  22813  xrsmopn  22824  metdcn2  22851  metdscn2  22869  bndth  22966  ovolunlem1a  23473  ovolunlem1  23474  ovoliunlem1  23479  ovoliun  23482  ovolicc2lem4  23497  voliunlem2  23528  voliunlem3  23529  opnmblALT  23580  vitalilem4  23588  mbfimaopnlem  23632  itg2le  23716  itg2seq  23719  dvfsumrlim  24004  itgsubst  24022  mdegleb  24034  mdeglt  24035  mdegldg  24036  mdegxrcl  24037  mdegcl  24039  mdegaddle  24044  mdegmullem  24048  deg1mul3le  24086  ig1pdvds  24146  aannenlem2  24294  taylfval  24323  radcnvcl  24381  radcnvlt1  24382  radcnvle  24384  xrlimcnp  24905  nmoxr  27946  nmooge0  27947  nmoolb  27951  nmoubi  27952  nmlno0lem  27973  nmopxr  29050  nmfnxr  29063  nmoplb  29091  nmopub  29092  nmfnlb  29108  nmfnleub  29109  nmlnop0iALT  29179  nmopun  29198  branmfn  29289  pjnmopi  29332  xlt2addrd  29847  xreceu  29952  rexdiv  29956  xrsmulgzz  30000  esumcst  30447  icorempt2  33512  mblfinlem2  33757  itg2addnc  33773  prdsbnd  33900  rrnequiv  33942  hbtlem2  38192  binomcxplemdvbinom  39049  binomcxplemcvg  39050  binomcxplemnotnn0  39052  suplesup  40032  frexr  40081  zssxr  40097  ssrexr  40135  uzxrd  40168  supminfxr  40170  rpssxr  40187  elicores  40237  ressiocsup  40258  ressioosup  40259  ressiooinf  40261  uzinico  40264  limsupre  40350  limsupresico  40409  limsuppnfdlem  40410  limsupmnflem  40429  limsupvaluz2  40447  supcnvlimsup  40449  liminfresico  40480  volicoff  40688  volicofmpt  40690  fourierdlem52  40851  fourierdlem103  40902  fourierdlem104  40903  etransclem48  40975  ioorrnopnlem  41000  fsumlesge0  41070  sge0cl  41074  sge0supre  41082  sge0less  41085  sge0split  41102  sge0seq  41139  hoicvr  41241  volicorescl  41246  ovolval2lem  41336  ovolval5lem2  41346  ovnovollem1  41349  ovnovollem2  41350  iinhoiicclem  41366  iunhoiioolem  41368  iccvonmbllem  41371  vonioolem2  41374  vonioo  41375  vonicclem2  41377  vonicc  41378  pimdecfgtioc  41404  pimincfltioc  41405  pimdecfgtioo  41406  pimincfltioo  41407  smflimsuplem4  41508
  Copyright terms: Public domain W3C validator