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

Theorem ressxr 10275
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 3919 . 2 ℝ ⊆ (ℝ ∪ {+∞, -∞})
2 df-xr 10270 . 2 * = (ℝ ∪ {+∞, -∞})
31, 2sseqtr4i 3779 1 ℝ ⊆ ℝ*
Colors of variables: wff setvar class
Syntax hints:  cun 3713  wss 3715  {cpr 4323  cr 10127  +∞cpnf 10263  -∞cmnf 10264  *cxr 10265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-un 3720  df-in 3722  df-ss 3729  df-xr 10270
This theorem is referenced by:  rexpssxrxp  10276  rexr  10277  0xr  10278  rexrd  10281  ltrelxr  10291  supxrre  12350  supxrbnd  12351  supxrgtmnf  12352  supxrre1  12353  supxrre2  12354  infxrre  12359  iooval2  12401  fzval2  12522  uzsup  12856  hashxrcl  13340  seqcoll  13440  limsupval2  14410  limsupgre  14411  limsupbnd2  14413  rlimuni  14480  rlimcld2  14508  rlimno1  14583  isercolllem2  14595  isercoll  14597  caucvgrlem  14602  summolem2a  14645  prodmolem2a  14863  ramtlecl  15906  ramxrcl  15923  ismet2  22339  prdsmet  22376  qtopbas  22764  tgqioo  22804  re2ndc  22805  xrsmopn  22816  metdcn2  22843  metdscn2  22861  bndth  22958  ovolunlem1a  23464  ovolunlem1  23465  ovoliunlem1  23470  ovoliun  23473  ovolicc2lem4  23488  voliunlem2  23519  voliunlem3  23520  opnmblALT  23571  vitalilem4  23579  mbfimaopnlem  23621  itg2le  23705  itg2seq  23708  dvfsumrlim  23993  itgsubst  24011  mdegleb  24023  mdeglt  24024  mdegldg  24025  mdegxrcl  24026  mdegcl  24028  mdegaddle  24033  mdegmullem  24037  deg1mul3le  24075  ig1pdvds  24135  aannenlem2  24283  taylfval  24312  radcnvcl  24370  radcnvlt1  24371  radcnvle  24373  xrlimcnp  24894  nmoxr  27930  nmooge0  27931  nmoolb  27935  nmoubi  27936  nmlno0lem  27957  nmopxr  29034  nmfnxr  29047  nmoplb  29075  nmopub  29076  nmfnlb  29092  nmfnleub  29093  nmlnop0iALT  29163  nmopun  29182  branmfn  29273  pjnmopi  29316  xlt2addrd  29832  xreceu  29939  rexdiv  29943  xrsmulgzz  29987  esumcst  30434  icorempt2  33510  mblfinlem2  33760  itg2addnc  33777  prdsbnd  33905  rrnequiv  33947  hbtlem2  38196  binomcxplemdvbinom  39054  binomcxplemcvg  39055  binomcxplemnotnn0  39057  suplesup  40053  frexr  40102  zssxr  40119  ssrexr  40157  uzxrd  40190  supminfxr  40192  rpssxr  40209  elicores  40263  ressiocsup  40284  ressioosup  40285  ressiooinf  40287  uzinico  40290  limsupre  40376  limsupresico  40435  limsuppnfdlem  40436  limsupmnflem  40455  limsupvaluz2  40473  supcnvlimsup  40475  liminfresico  40506  volicoff  40715  volicofmpt  40717  fourierdlem52  40878  fourierdlem103  40929  fourierdlem104  40930  etransclem48  41002  ioorrnopnlem  41027  fsumlesge0  41097  sge0cl  41101  sge0supre  41109  sge0less  41112  sge0split  41129  sge0seq  41166  hoicvr  41268  volicorescl  41273  ovolval2lem  41363  ovolval5lem2  41373  ovnovollem1  41376  ovnovollem2  41377  iinhoiicclem  41393  iunhoiioolem  41395  iccvonmbllem  41398  vonioolem2  41401  vonioo  41402  vonicclem2  41404  vonicc  41405  pimdecfgtioc  41431  pimincfltioc  41432  pimdecfgtioo  41433  pimincfltioo  41434  smflimsuplem4  41535
  Copyright terms: Public domain W3C validator