Theorem pnfxr 11199

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 4119	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11198	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4706	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3918	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11183	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2835	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2114   ∪ cun 3887  {cpr 4569  ℝcr 11037  +∞cpnf 11176  -∞cmnf 11177  ℝ^*cxr 11178

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pow 5307  ax-un 7689  ax-cnex 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-pw 4543  df-sn 4568  df-pr 4570  df-uni 4851  df-pnf 11181  df-xr 11183

This theorem is referenced by:  pnfnemnf  11200  xnn0xr  12515  xrltnr  13070  ltpnf  13071  mnfltpnf  13077  pnfnlt  13079  pnfge  13081  nltpnft  13116  xgepnf  13117  xrre  13121  xrre2  13122  xnegcl  13165  xaddf  13176  xaddpnf1  13178  xaddpnf2  13179  pnfaddmnf  13182  mnfaddpnf  13183  xaddass2  13202  xlt2add  13212  xsubge0  13213  xmulneg1  13221  xmulf  13224  xmulpnf1  13226  xmulpnf2  13227  xmulmnf1  13228  xmulpnf1n  13230  xlemul1a  13240  xadddilem  13246  xadddi2  13249  xrsupsslem  13259  xrinfmsslem  13260  supxrpnf  13270  supxrunb1  13271  supxrunb2  13272  supxrbnd  13280  xrinf0  13291  dfrp2  13347  elicore  13351  elioc2  13362  elico2  13363  elicc2  13364  ioomax  13375  iccmax  13376  ioopos  13377  elioopnf  13396  elicopnf  13398  unirnioo  13402  xrge0neqmnf  13405  elxrge0  13410  difreicc  13437  xnn0xrge0  13459  ioopnfsup  13823  icopnfsup  13824  xrsup  13827  hashbnd  14298  hashnnn0genn0  14305  hashxrcl  14319  hashdomi  14342  sgnpnf  15055  rexico  15316  limsupgre  15443  rlim3  15460  fprodge0  15958  fprodge1  15960  pcxcl  16832  pc2dvds  16850  pcadd  16860  ramxrcl  16988  ramubcl  16989  xrsnsgrp  21388  xrsdsreclblem  21393  rge0srg  21418  leordtvallem1  23175  leordtval2  23177  lecldbas  23184  pnfnei  23185  mnfnei  23186  xblpnfps  24360  xblpnf  24361  xblss2ps  24366  blssec  24400  blpnfctr  24401  nmoix  24694  icopnfcld  24732  iocmnfcld  24733  xrtgioo  24772  reconnlem1  24792  xrge0tsms  24800  metdstri  24817  iccpnfcnv  24911  ovolf  25449  ovolicopnf  25491  ovolre  25492  volsup  25523  ioombl1lem4  25528  icombl1  25530  icombl  25531  ioombl  25532  uniioombllem1  25548  mbfdm  25593  ismbfd  25606  mbfmax  25616  ismbf3d  25621  itg2ge0  25702  lhop2  25982  dvfsumlem2  25994  dvfsumrlim  25998  dvfsumrlim2  25999  taylfvallem1  26322  taylfval  26324  tayl0  26327  radcnvcl  26382  radcnvle  26385  psercnlem1  26390  logccv  26627  rlimcnp  26929  rlimcnp2  26930  xrlimcnp  26932  logfacbnd3  27186  chebbnd1  27435  chebbnd2  27440  dchrisumlem3  27454  log2sumbnd  27507  pntpbnd1  27549  pntibndlem2  27554  pntlemb  27560  pntleme  27571  pnt  27577  upgrfi  29160  topnfbey  30539  isblo3i  30872  xrge0infss  32833  xrdifh  32853  hashxpe  32880  elxrge02  32991  xdivpnfrp  32992  xrge0addass  33076  xrge0addgt0  33077  xrge0adddir  33078  xrge0npcan  33080  fsumrp0cl  33081  xrge0tsmsd  33134  pnfinf  33244  xrnarchi  33245  xrge0slmod  33408  unitssxrge0  34044  tpr2rico  34056  xrge0iifcnv  34077  xrge0iifiso  34079  xrge0iifhom  34081  xrge0mulc1cn  34085  pnfneige0  34095  lmxrge0  34096  esumle  34202  esumlef  34206  esumcst  34207  esumpr2  34211  esumpinfval  34217  esumpinfsum  34221  esumpcvgval  34222  hashf2  34228  esumcvg  34230  esumcvgsum  34232  voliune  34373  volfiniune  34374  ddemeas  34380  sxbrsigalem0  34415  sxbrsigalem2  34430  oms0  34441  sibfinima  34483  sitmcl  34495  probmeasb  34574  orvcgteel  34612  dstfrvclim1  34622  signsply0  34695  chtvalz  34773  hgt750lemf  34797  iooelexlt  37678  mbfposadd  37988  itg2addnclem2  37993  ftc1anclem5  38018  asindmre  38024  dvasin  38025  dvacos  38026  aks4d1p1p6  42512  readvrec2  42793  readvrec  42794  dvconstbi  44761  rfcnpre3  45464  absfico  45647  xadd0ge  45752  xrgepnfd  45761  xrge0nemnfd  45762  supxrgere  45763  supxrgelem  45767  supxrge  45768  xralrple2  45784  infxr  45796  infleinflem2  45800  xrralrecnnge  45819  infxrpnf  45874  xrpnf  45913  iocopn  45950  pnfel0pnf  45958  ge0xrre  45961  ge0lere  45962  ressiooinf  45987  uzinico  45989  uzubioo  45995  fsumge0cl  46003  limcicciooub  46065  limsupre  46069  limcresiooub  46070  limcleqr  46072  limsupresre  46124  limsupresico  46128  limsuppnfdlem  46129  limsuppnflem  46138  limsupmnflem  46148  liminfresico  46199  limsup10exlem  46200  liminflelimsuplem  46203  liminflelimsupuz  46213  limsupub2  46240  liminflbuz2  46243  liminflimsupxrre  46245  xlimpnfvlem2  46265  xlimliminflimsup  46290  icccncfext  46315  iblsplit  46394  itgsubsticclem  46403  fourierdlem31  46566  fourierdlem33  46568  fourierdlem46  46580  fourierdlem47  46581  fourierdlem48  46582  fourierdlem49  46583  fourierdlem65  46599  fourierdlem73  46607  fourierdlem75  46609  fourierdlem85  46619  fourierdlem88  46622  fourierdlem95  46629  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  fourierdlem107  46641  fourierdlem109  46643  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  fouriersw  46659  ioorrnopnxrlem  46734  sge0val  46794  fge0iccico  46798  gsumge0cl  46799  sge0sn  46807  sge0tsms  46808  sge0cl  46809  sge0f1o  46810  sge0ge0  46812  sge0repnf  46814  sge0fsum  46815  sge0pr  46822  sge0prle  46829  sge0split  46837  sge0p1  46842  sge0iunmptlemre  46843  sge0rpcpnf  46849  sge0rernmpt  46850  sge0isum  46855  sge0ad2en  46859  sge0xaddlem1  46861  sge0xaddlem2  46862  sge0uzfsumgt  46872  sge0seq  46874  sge0reuz  46875  voliunsge0lem  46900  meage0  46903  meassre  46905  meaiuninclem  46908  omessre  46938  omeiunltfirp  46947  carageniuncllem2  46950  carageniuncl  46951  omege0  46961  hoiprodcl  46975  hoicvrrex  46984  ovnpnfelsup  46987  ovnlerp  46990  ovnf  46991  ovn0lem  46993  ovnsubaddlem1  46998  hoiprodcl3  47008  hoidmvcl  47010  sge0hsphoire  47017  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem4  47026  hoidmvlelem5  47027  ovnhoilem1  47029  volicorege0  47065  ovolval5lem1  47080  pimgtpnf2f  47133  pimiooltgt  47138  smfliminflem  47258  rehalfge1  47787  rrxsphere  49224  itscnhlinecirc02p  49261