Theorem pnfxr 11264

Description: Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)

Assertion

Ref	Expression
pnfxr	⊢ +∞ ∈ ℝ*

Proof of Theorem pnfxr

Step	Hyp	Ref	Expression
1		ssun2 4133	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11263	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4729	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3935	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11248	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2862	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2143   ∪ cun 3904  {cpr 4592  ℝcr 11100  +∞cpnf 11241  -∞cmnf 11242  ℝ^*cxr 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-un 7734  ax-cnex 11157

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-pw 4565  df-sn 4591  df-pr 4593  df-uni 4874  df-pnf 11246  df-xr 11248

This theorem is referenced by:  pnfnemnf  11265  xnn0xr  12583  xrltnr  13145  ltpnf  13146  mnfltpnf  13152  pnfnlt  13154  pnfge  13156  nltpnft  13191  xgepnf  13192  xrre  13196  xrre2  13197  xnegcl  13240  xaddf  13251  xaddpnf1  13253  xaddpnf2  13254  pnfaddmnf  13257  mnfaddpnf  13258  xaddass2  13277  xlt2add  13287  xsubge0  13288  xmulneg1  13296  xmulf  13299  xmulpnf1  13301  xmulpnf2  13302  xmulmnf1  13303  xmulpnf1n  13305  xlemul1a  13315  xadddilem  13321  xadddi2  13324  xrsupsslem  13334  xrinfmsslem  13335  supxrpnf  13345  supxrunb1  13346  supxrunb2  13347  supxrbnd  13355  xrinf0  13366  dfrp2  13422  elicore  13426  elioc2  13437  elico2  13438  elicc2  13439  ioomax  13450  iccmax  13451  ioopos  13452  elioopnf  13471  elicopnf  13473  unirnioo  13477  xrge0neqmnf  13480  elxrge0  13485  difreicc  13512  xnn0xrge0  13534  ioopnfsup  13899  icopnfsup  13900  xrsup  13903  hashbnd  14374  hashnnn0genn0  14381  hashxrcl  14395  hashdomi  14418  sgnpnf  15132  rexico  15407  limsupgre  15534  rlim3  15551  fprodge0  16049  fprodge1  16051  pcxcl  16922  pc2dvds  16940  pcadd  16950  ramxrcl  17078  ramubcl  17079  xrsnsgrp  21539  xrsdsreclblem  21544  rge0srg  21569  leordtvallem1  23348  leordtval2  23350  lecldbas  23357  pnfnei  23358  mnfnei  23359  xblpnfps  24533  xblpnf  24534  xblss2ps  24539  blssec  24573  blpnfctr  24574  nmoix  24867  icopnfcld  24905  iocmnfcld  24906  xrtgioo  24945  reconnlem1  24965  xrge0tsms  24973  metdstri  24990  iccpnfcnv  25084  ovolf  25622  ovolicopnf  25664  ovolre  25665  volsup  25696  ioombl1lem4  25701  icombl1  25703  icombl  25704  ioombl  25705  uniioombllem1  25721  mbfdm  25766  ismbfd  25779  mbfmax  25789  ismbf3d  25794  itg2ge0  25875  lhop2  26155  dvfsumlem2  26167  dvfsumrlim  26171  dvfsumrlim2  26172  taylfvallem1  26501  taylfval  26503  tayl0  26506  radcnvcl  26561  radcnvle  26564  psercnlem1  26569  logccv  26809  rlimcnp  27111  rlimcnp2  27112  xrlimcnp  27114  logfacbnd3  27368  chebbnd1  27617  chebbnd2  27622  dchrisumlem3  27636  log2sumbnd  27689  pntpbnd1  27731  pntibndlem2  27736  pntlemb  27742  pntleme  27753  pnt  27759  upgrfi  29422  topnfbey  30801  isblo3i  31134  xrge0infss  33086  xrdifh  33106  hashxpe  33133  elxrge02  33232  xdivpnfrp  33233  xrge0addass  33317  xrge0addgt0  33318  xrge0adddir  33319  xrge0npcan  33321  fsumrp0cl  33322  xrge0tsmsd  33374  pnfinf  33484  xrnarchi  33485  xrge0slmod  33649  unitssxrge0  34271  tpr2rico  34283  xrge0iifcnv  34304  xrge0iifiso  34306  xrge0iifhom  34308  xrge0mulc1cn  34312  pnfneige0  34322  lmxrge0  34323  esumle  34429  esumlef  34433  esumcst  34434  esumpr2  34438  esumpinfval  34444  esumpinfsum  34448  esumpcvgval  34449  hashf2  34455  esumcvg  34457  esumcvgsum  34459  voliune  34600  volfiniune  34601  ddemeas  34607  sxbrsigalem0  34642  sxbrsigalem2  34657  oms0  34668  sibfinima  34710  sitmcl  34722  probmeasb  34801  orvcgteel  34839  dstfrvclim1  34849  signsply0  34919  chtvalz  34997  hgt750lemf  35021  iooelexlt  37989  mbfposadd  38299  itg2addnclem2  38304  ftc1anclem5  38329  asindmre  38335  dvasin  38336  dvacos  38337  aks4d1p1p6  42821  readvrec2  43103  readvrec  43104  dvconstbi  45027  rfcnpre3  45736  absfico  45917  xadd0ge  46021  xrgepnfd  46030  xrge0nemnfd  46031  supxrgere  46032  supxrgelem  46036  supxrge  46037  xralrple2  46053  infxr  46065  infleinflem2  46069  xrralrecnnge  46088  infxrpnf  46143  xrpnf  46182  iocopn  46219  pnfel0pnf  46227  ge0xrre  46230  ge0lere  46231  ressiooinf  46256  uzinico  46258  uzubioo  46264  fsumge0cl  46272  limcicciooub  46334  limsupre  46338  limcresiooub  46339  limcleqr  46341  limsupresre  46393  limsupresico  46397  limsuppnfdlem  46398  limsuppnflem  46407  limsupmnflem  46417  liminfresico  46468  limsup10exlem  46469  liminflelimsuplem  46472  liminflelimsupuz  46482  limsupub2  46509  liminflbuz2  46512  liminflimsupxrre  46514  xlimpnfvlem2  46534  xlimliminflimsup  46559  icccncfext  46584  iblsplit  46663  itgsubsticclem  46672  fourierdlem31  46835  fourierdlem33  46837  fourierdlem46  46849  fourierdlem47  46850  fourierdlem48  46851  fourierdlem49  46852  fourierdlem65  46868  fourierdlem73  46876  fourierdlem75  46878  fourierdlem85  46888  fourierdlem88  46891  fourierdlem95  46898  fourierdlem97  46900  fourierdlem103  46906  fourierdlem104  46907  fourierdlem107  46910  fourierdlem109  46912  fourierdlem111  46914  fourierdlem112  46915  fourierdlem113  46916  fouriersw  46928  ioorrnopnxrlem  47003  sge0val  47063  fge0iccico  47067  gsumge0cl  47068  sge0sn  47076  sge0tsms  47077  sge0cl  47078  sge0f1o  47079  sge0ge0  47081  sge0repnf  47083  sge0fsum  47084  sge0pr  47091  sge0prle  47098  sge0split  47106  sge0p1  47111  sge0iunmptlemre  47112  sge0rpcpnf  47118  sge0rernmpt  47119  sge0isum  47124  sge0ad2en  47128  sge0xaddlem1  47130  sge0xaddlem2  47131  sge0uzfsumgt  47141  sge0seq  47143  sge0reuz  47144  voliunsge0lem  47169  meage0  47172  meassre  47174  meaiuninclem  47177  omessre  47207  omeiunltfirp  47216  carageniuncllem2  47219  carageniuncl  47220  omege0  47230  hoiprodcl  47244  hoicvrrex  47253  ovnpnfelsup  47256  ovnlerp  47259  ovnf  47260  ovn0lem  47262  ovnsubaddlem1  47267  hoiprodcl3  47277  hoidmvcl  47279  sge0hsphoire  47286  hoidmv1lelem1  47288  hoidmv1lelem2  47289  hoidmv1lelem3  47290  hoidmv1le  47291  hoidmvlelem1  47292  hoidmvlelem4  47295  hoidmvlelem5  47296  ovnhoilem1  47298  volicorege0  47334  ovolval5lem1  47349  pimgtpnf2f  47402  pimiooltgt  47407  smfliminflem  47527  rehalfge1  48059  rrxsphere  49511  itscnhlinecirc02p  49548