Theorem pnfxr 10960

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 4103	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 10959	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4695	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3914	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 10944	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2838	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2108   ∪ cun 3881  {cpr 4560  ℝcr 10801  +∞cpnf 10937  -∞cmnf 10938  ℝ^*cxr 10939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-pow 5283  ax-un 7566  ax-cnex 10858

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-pw 4532  df-sn 4559  df-pr 4561  df-uni 4837  df-pnf 10942  df-xr 10944

This theorem is referenced by:  pnfnemnf  10961  xnn0xr  12240  xrltnr  12784  ltpnf  12785  mnfltpnf  12791  pnfnlt  12793  pnfge  12795  nltpnft  12827  xgepnf  12828  xrre  12832  xrre2  12833  xnegcl  12876  xaddf  12887  xaddpnf1  12889  xaddpnf2  12890  pnfaddmnf  12893  mnfaddpnf  12894  xaddass2  12913  xlt2add  12923  xsubge0  12924  xmulneg1  12932  xmulf  12935  xmulpnf1  12937  xmulpnf2  12938  xmulmnf1  12939  xmulpnf1n  12941  xlemul1a  12951  xadddilem  12957  xadddi2  12960  xrsupsslem  12970  xrinfmsslem  12971  supxrpnf  12981  supxrunb1  12982  supxrunb2  12983  supxrbnd  12991  xrinf0  13001  dfrp2  13057  elicore  13060  elioc2  13071  elico2  13072  elicc2  13073  ioomax  13083  iccmax  13084  ioopos  13085  elioopnf  13104  elicopnf  13106  unirnioo  13110  xrge0neqmnf  13113  elxrge0  13118  difreicc  13145  xnn0xrge0  13167  ioopnfsup  13512  icopnfsup  13513  xrsup  13516  hashbnd  13978  hashnnn0genn0  13985  hashxrcl  14000  hashdomi  14023  sgnpnf  14732  rexico  14993  limsupgre  15118  rlim3  15135  fprodge0  15631  fprodge1  15633  pcxcl  16490  pc2dvds  16508  pcadd  16518  ramxrcl  16646  ramubcl  16647  xrsnsgrp  20546  xrsdsreclblem  20556  rge0srg  20581  leordtvallem1  22269  leordtval2  22271  lecldbas  22278  pnfnei  22279  mnfnei  22280  xblpnfps  23456  xblpnf  23457  xblss2ps  23462  blssec  23496  blpnfctr  23497  nmoix  23799  icopnfcld  23837  iocmnfcld  23838  xrtgioo  23875  reconnlem1  23895  xrge0tsms  23903  metdstri  23920  iccpnfcnv  24013  ovolf  24551  ovolicopnf  24593  ovolre  24594  volsup  24625  ioombl1lem4  24630  icombl1  24632  icombl  24633  ioombl  24634  uniioombllem1  24650  mbfdm  24695  ismbfd  24708  mbfmax  24718  ismbf3d  24723  itg2ge0  24805  lhop2  25084  dvfsumlem2  25096  dvfsumrlim  25100  dvfsumrlim2  25101  taylfvallem1  25421  taylfval  25423  tayl0  25426  radcnvcl  25481  radcnvle  25484  psercnlem1  25489  logccv  25723  rlimcnp  26020  rlimcnp2  26021  xrlimcnp  26023  logfacbnd3  26276  chebbnd1  26525  chebbnd2  26530  dchrisumlem3  26544  log2sumbnd  26597  pntpbnd1  26639  pntibndlem2  26644  pntlemb  26650  pntleme  26661  pnt  26667  upgrfi  27364  topnfbey  28734  isblo3i  29064  xrge0infss  30985  xrdifh  31003  hashxpe  31029  elxrge02  31108  xdivpnfrp  31109  xrge0addass  31201  xrge0addgt0  31202  xrge0adddir  31203  xrge0npcan  31205  fsumrp0cl  31206  xrge0tsmsd  31219  pnfinf  31339  xrnarchi  31340  xrge0slmod  31450  unitssxrge0  31752  tpr2rico  31764  xrge0iifcnv  31785  xrge0iifiso  31787  xrge0iifhom  31789  xrge0mulc1cn  31793  pnfneige0  31803  lmxrge0  31804  esumle  31926  esumlef  31930  esumcst  31931  esumpr2  31935  esumpinfval  31941  esumpinfsum  31945  esumpcvgval  31946  hashf2  31952  esumcvg  31954  esumcvgsum  31956  voliune  32097  volfiniune  32098  ddemeas  32104  sxbrsigalem0  32138  sxbrsigalem2  32153  oms0  32164  sibfinima  32206  sitmcl  32218  probmeasb  32297  orvcgteel  32334  dstfrvclim1  32344  signsply0  32430  chtvalz  32509  hgt750lemf  32533  iooelexlt  35460  mbfposadd  35751  itg2addnclem2  35756  ftc1anclem5  35781  asindmre  35787  dvasin  35788  dvacos  35789  aks4d1p1p6  40009  dvconstbi  41841  rfcnpre3  42465  absfico  42647  xadd0ge  42749  xrgepnfd  42760  xrge0nemnfd  42761  supxrgere  42762  supxrgelem  42766  supxrge  42767  xralrple2  42783  infxr  42796  infleinflem2  42800  xrralrecnnge  42820  infxrpnf  42876  xrpnf  42916  iocopn  42948  pnfel0pnf  42956  ge0xrre  42959  ge0lere  42960  ressiooinf  42985  uzinico  42988  uzubioo  42995  fsumge0cl  43004  limcicciooub  43068  limsupre  43072  limcresiooub  43073  limcleqr  43075  limsupresre  43127  limsupresico  43131  limsuppnfdlem  43132  limsuppnflem  43141  limsupmnflem  43151  liminfresico  43202  limsup10exlem  43203  liminflelimsuplem  43206  liminflelimsupuz  43216  limsupub2  43243  liminflbuz2  43246  liminflimsupxrre  43248  xlimpnfvlem2  43268  xlimliminflimsup  43293  icccncfext  43318  iblsplit  43397  itgsubsticclem  43406  fourierdlem31  43569  fourierdlem33  43571  fourierdlem46  43583  fourierdlem47  43584  fourierdlem48  43585  fourierdlem49  43586  fourierdlem65  43602  fourierdlem73  43610  fourierdlem75  43612  fourierdlem85  43622  fourierdlem88  43625  fourierdlem95  43632  fourierdlem97  43634  fourierdlem103  43640  fourierdlem104  43641  fourierdlem107  43644  fourierdlem109  43646  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  fouriersw  43662  ioorrnopnxrlem  43737  sge0val  43794  fge0iccico  43798  gsumge0cl  43799  sge0sn  43807  sge0tsms  43808  sge0cl  43809  sge0f1o  43810  sge0ge0  43812  sge0repnf  43814  sge0fsum  43815  sge0pr  43822  sge0prle  43829  sge0split  43837  sge0p1  43842  sge0iunmptlemre  43843  sge0rpcpnf  43849  sge0rernmpt  43850  sge0isum  43855  sge0ad2en  43859  sge0xaddlem1  43861  sge0xaddlem2  43862  sge0uzfsumgt  43872  sge0seq  43874  sge0reuz  43875  voliunsge0lem  43900  meage0  43903  meassre  43905  meaiuninclem  43908  omessre  43938  omeiunltfirp  43947  carageniuncllem2  43950  carageniuncl  43951  omege0  43961  hoiprodcl  43975  hoicvrrex  43984  ovnpnfelsup  43987  ovnlerp  43990  ovnf  43991  ovn0lem  43993  ovnsubaddlem1  43998  hoiprodcl3  44008  hoidmvcl  44010  sge0hsphoire  44017  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem4  44026  hoidmvlelem5  44027  ovnhoilem1  44029  volicorege0  44065  ovolval5lem1  44080  pimgtpnf2  44131  pimiooltgt  44135  smfliminflem  44250  rrxsphere  45982  itscnhlinecirc02p  46019