Theorem pnfxr 10684

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 4100	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 10683	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4658	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3912	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 10668	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2889	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2111   ∪ cun 3879  {cpr 4527  ℝcr 10525  +∞cpnf 10661  -∞cmnf 10662  ℝ^*cxr 10663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-pow 5231  ax-un 7441  ax-cnex 10582

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-pw 4499  df-sn 4526  df-pr 4528  df-uni 4801  df-pnf 10666  df-xr 10668

This theorem is referenced by:  pnfnemnf  10685  xnn0xr  11960  xrltnr  12502  ltpnf  12503  mnfltpnf  12509  pnfnlt  12511  pnfge  12513  nltpnft  12545  xgepnf  12546  xrre  12550  xrre2  12551  xnegcl  12594  xaddf  12605  xaddpnf1  12607  xaddpnf2  12608  pnfaddmnf  12611  mnfaddpnf  12612  xaddass2  12631  xlt2add  12641  xsubge0  12642  xmulneg1  12650  xmulf  12653  xmulpnf1  12655  xmulpnf2  12656  xmulmnf1  12657  xmulpnf1n  12659  xlemul1a  12669  xadddilem  12675  xadddi2  12678  xrsupsslem  12688  xrinfmsslem  12689  supxrpnf  12699  supxrunb1  12700  supxrunb2  12701  supxrbnd  12709  xrinf0  12719  elicore  12777  elioc2  12788  elico2  12789  elicc2  12790  ioomax  12800  iccmax  12801  ioopos  12802  elioopnf  12821  elicopnf  12823  unirnioo  12827  xrge0neqmnf  12830  elxrge0  12835  difreicc  12862  xnn0xrge0  12884  ioopnfsup  13227  icopnfsup  13228  xrsup  13231  hashbnd  13692  hashnnn0genn0  13699  hashxrcl  13714  hashdomi  13737  sgnpnf  14444  rexico  14705  limsupgre  14830  rlim3  14847  fprodge0  15339  fprodge1  15341  pcxcl  16187  pc2dvds  16205  pcadd  16215  ramxrcl  16343  ramubcl  16344  xrsnsgrp  20127  xrsdsreclblem  20137  rge0srg  20162  leordtvallem1  21815  leordtval2  21817  lecldbas  21824  pnfnei  21825  mnfnei  21826  xblpnfps  23002  xblpnf  23003  xblss2ps  23008  blssec  23042  blpnfctr  23043  nmoix  23335  icopnfcld  23373  iocmnfcld  23374  xrtgioo  23411  reconnlem1  23431  xrge0tsms  23439  metdstri  23456  iccpnfcnv  23549  ovolf  24086  ovolicopnf  24128  ovolre  24129  volsup  24160  ioombl1lem4  24165  icombl1  24167  icombl  24168  ioombl  24169  uniioombllem1  24185  mbfdm  24230  ismbfd  24243  mbfmax  24253  ismbf3d  24258  itg2ge0  24339  lhop2  24618  dvfsumlem2  24630  dvfsumrlim  24634  dvfsumrlim2  24635  taylfvallem1  24952  taylfval  24954  tayl0  24957  radcnvcl  25012  radcnvle  25015  psercnlem1  25020  logccv  25254  rlimcnp  25551  rlimcnp2  25552  xrlimcnp  25554  logfacbnd3  25807  chebbnd1  26056  chebbnd2  26061  dchrisumlem3  26075  log2sumbnd  26128  pntpbnd1  26170  pntibndlem2  26175  pntlemb  26181  pntleme  26192  pnt  26198  upgrfi  26884  topnfbey  28254  isblo3i  28584  xrge0infss  30510  dfrp2  30517  xrdifh  30529  hashxpe  30555  elxrge02  30634  xdivpnfrp  30635  xrge0addass  30724  xrge0addgt0  30725  xrge0adddir  30726  xrge0npcan  30728  fsumrp0cl  30729  xrge0tsmsd  30742  pnfinf  30862  xrnarchi  30863  xrge0slmod  30968  unitssxrge0  31253  tpr2rico  31265  xrge0iifcnv  31286  xrge0iifiso  31288  xrge0iifhom  31290  xrge0mulc1cn  31294  pnfneige0  31304  lmxrge0  31305  esumle  31427  esumlef  31431  esumcst  31432  esumpr2  31436  esumpinfval  31442  esumpinfsum  31446  esumpcvgval  31447  hashf2  31453  esumcvg  31455  esumcvgsum  31457  voliune  31598  volfiniune  31599  ddemeas  31605  sxbrsigalem0  31639  sxbrsigalem2  31654  oms0  31665  sibfinima  31707  sitmcl  31719  probmeasb  31798  orvcgteel  31835  dstfrvclim1  31845  signsply0  31931  chtvalz  32010  hgt750lemf  32034  iooelexlt  34779  mbfposadd  35104  itg2addnclem2  35109  ftc1anclem5  35134  asindmre  35140  dvasin  35141  dvacos  35142  dvconstbi  41038  rfcnpre3  41662  absfico  41847  xadd0ge  41952  xrgepnfd  41963  xrge0nemnfd  41964  supxrgere  41965  supxrgelem  41969  supxrge  41970  xralrple2  41986  infxr  41999  infleinflem2  42003  xrralrecnnge  42026  infxrpnf  42084  xrpnf  42125  iocopn  42157  pnfel0pnf  42165  ge0xrre  42168  ge0lere  42169  ressiooinf  42194  uzinico  42197  uzubioo  42204  fsumge0cl  42215  limcicciooub  42279  limsupre  42283  limcresiooub  42284  limcleqr  42286  limsupresre  42338  limsupresico  42342  limsuppnfdlem  42343  limsuppnflem  42352  limsupmnflem  42362  liminfresico  42413  limsup10exlem  42414  liminflelimsuplem  42417  liminflelimsupuz  42427  limsupub2  42454  liminflbuz2  42457  liminflimsupxrre  42459  xlimpnfvlem2  42479  xlimliminflimsup  42504  icccncfext  42529  iblsplit  42608  itgsubsticclem  42617  fourierdlem31  42780  fourierdlem33  42782  fourierdlem46  42794  fourierdlem47  42795  fourierdlem48  42796  fourierdlem49  42797  fourierdlem65  42813  fourierdlem73  42821  fourierdlem75  42823  fourierdlem85  42833  fourierdlem88  42836  fourierdlem95  42843  fourierdlem97  42845  fourierdlem103  42851  fourierdlem104  42852  fourierdlem107  42855  fourierdlem109  42857  fourierdlem111  42859  fourierdlem112  42860  fourierdlem113  42861  fouriersw  42873  ioorrnopnxrlem  42948  sge0val  43005  fge0iccico  43009  gsumge0cl  43010  sge0sn  43018  sge0tsms  43019  sge0cl  43020  sge0f1o  43021  sge0ge0  43023  sge0repnf  43025  sge0fsum  43026  sge0pr  43033  sge0prle  43040  sge0split  43048  sge0p1  43053  sge0iunmptlemre  43054  sge0rpcpnf  43060  sge0rernmpt  43061  sge0isum  43066  sge0ad2en  43070  sge0xaddlem1  43072  sge0xaddlem2  43073  sge0uzfsumgt  43083  sge0seq  43085  sge0reuz  43086  voliunsge0lem  43111  meage0  43114  meassre  43116  meaiuninclem  43119  omessre  43149  omeiunltfirp  43158  carageniuncllem2  43161  carageniuncl  43162  omege0  43172  hoiprodcl  43186  hoicvrrex  43195  ovnpnfelsup  43198  ovnlerp  43201  ovnf  43202  ovn0lem  43204  ovnsubaddlem1  43209  hoiprodcl3  43219  hoidmvcl  43221  sge0hsphoire  43228  hoidmv1lelem1  43230  hoidmv1lelem2  43231  hoidmv1lelem3  43232  hoidmv1le  43233  hoidmvlelem1  43234  hoidmvlelem4  43237  hoidmvlelem5  43238  ovnhoilem1  43240  volicorege0  43276  ovolval5lem1  43291  pimgtpnf2  43342  pimiooltgt  43346  smfliminflem  43461  rrxsphere  45162  itscnhlinecirc02p  45199