Theorem pnfxr 10733

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 4078	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 10732	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4655	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3889	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 10717	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2851	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2111   ∪ cun 3856  {cpr 4524  ℝcr 10574  +∞cpnf 10710  -∞cmnf 10711  ℝ^*cxr 10712

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 2729  ax-sep 5169  ax-pow 5234  ax-un 7459  ax-cnex 10631

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 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3863  df-in 3865  df-ss 3875  df-pw 4496  df-sn 4523  df-pr 4525  df-uni 4799  df-pnf 10715  df-xr 10717

This theorem is referenced by:  pnfnemnf  10734  xnn0xr  12011  xrltnr  12555  ltpnf  12556  mnfltpnf  12562  pnfnlt  12564  pnfge  12566  nltpnft  12598  xgepnf  12599  xrre  12603  xrre2  12604  xnegcl  12647  xaddf  12658  xaddpnf1  12660  xaddpnf2  12661  pnfaddmnf  12664  mnfaddpnf  12665  xaddass2  12684  xlt2add  12694  xsubge0  12695  xmulneg1  12703  xmulf  12706  xmulpnf1  12708  xmulpnf2  12709  xmulmnf1  12710  xmulpnf1n  12712  xlemul1a  12722  xadddilem  12728  xadddi2  12731  xrsupsslem  12741  xrinfmsslem  12742  supxrpnf  12752  supxrunb1  12753  supxrunb2  12754  supxrbnd  12762  xrinf0  12772  dfrp2  12828  elicore  12831  elioc2  12842  elico2  12843  elicc2  12844  ioomax  12854  iccmax  12855  ioopos  12856  elioopnf  12875  elicopnf  12877  unirnioo  12881  xrge0neqmnf  12884  elxrge0  12889  difreicc  12916  xnn0xrge0  12938  ioopnfsup  13281  icopnfsup  13282  xrsup  13285  hashbnd  13746  hashnnn0genn0  13753  hashxrcl  13768  hashdomi  13791  sgnpnf  14500  rexico  14761  limsupgre  14886  rlim3  14903  fprodge0  15395  fprodge1  15397  pcxcl  16252  pc2dvds  16270  pcadd  16280  ramxrcl  16408  ramubcl  16409  xrsnsgrp  20202  xrsdsreclblem  20212  rge0srg  20237  leordtvallem1  21910  leordtval2  21912  lecldbas  21919  pnfnei  21920  mnfnei  21921  xblpnfps  23097  xblpnf  23098  xblss2ps  23103  blssec  23137  blpnfctr  23138  nmoix  23431  icopnfcld  23469  iocmnfcld  23470  xrtgioo  23507  reconnlem1  23527  xrge0tsms  23535  metdstri  23552  iccpnfcnv  23645  ovolf  24182  ovolicopnf  24224  ovolre  24225  volsup  24256  ioombl1lem4  24261  icombl1  24263  icombl  24264  ioombl  24265  uniioombllem1  24281  mbfdm  24326  ismbfd  24339  mbfmax  24349  ismbf3d  24354  itg2ge0  24435  lhop2  24714  dvfsumlem2  24726  dvfsumrlim  24730  dvfsumrlim2  24731  taylfvallem1  25051  taylfval  25053  tayl0  25056  radcnvcl  25111  radcnvle  25114  psercnlem1  25119  logccv  25353  rlimcnp  25650  rlimcnp2  25651  xrlimcnp  25653  logfacbnd3  25906  chebbnd1  26155  chebbnd2  26160  dchrisumlem3  26174  log2sumbnd  26227  pntpbnd1  26269  pntibndlem2  26274  pntlemb  26280  pntleme  26291  pnt  26297  upgrfi  26983  topnfbey  28353  isblo3i  28683  xrge0infss  30607  xrdifh  30625  hashxpe  30651  elxrge02  30730  xdivpnfrp  30731  xrge0addass  30825  xrge0addgt0  30826  xrge0adddir  30827  xrge0npcan  30829  fsumrp0cl  30830  xrge0tsmsd  30843  pnfinf  30963  xrnarchi  30964  xrge0slmod  31069  unitssxrge0  31371  tpr2rico  31383  xrge0iifcnv  31404  xrge0iifiso  31406  xrge0iifhom  31408  xrge0mulc1cn  31412  pnfneige0  31422  lmxrge0  31423  esumle  31545  esumlef  31549  esumcst  31550  esumpr2  31554  esumpinfval  31560  esumpinfsum  31564  esumpcvgval  31565  hashf2  31571  esumcvg  31573  esumcvgsum  31575  voliune  31716  volfiniune  31717  ddemeas  31723  sxbrsigalem0  31757  sxbrsigalem2  31772  oms0  31783  sibfinima  31825  sitmcl  31837  probmeasb  31916  orvcgteel  31953  dstfrvclim1  31963  signsply0  32049  chtvalz  32128  hgt750lemf  32152  iooelexlt  35059  mbfposadd  35384  itg2addnclem2  35389  ftc1anclem5  35414  asindmre  35420  dvasin  35421  dvacos  35422  aks4d1p1p6  39639  dvconstbi  41411  rfcnpre3  42035  absfico  42217  xadd0ge  42320  xrgepnfd  42331  xrge0nemnfd  42332  supxrgere  42333  supxrgelem  42337  supxrge  42338  xralrple2  42354  infxr  42367  infleinflem2  42371  xrralrecnnge  42393  infxrpnf  42450  xrpnf  42491  iocopn  42523  pnfel0pnf  42531  ge0xrre  42534  ge0lere  42535  ressiooinf  42560  uzinico  42563  uzubioo  42570  fsumge0cl  42581  limcicciooub  42645  limsupre  42649  limcresiooub  42650  limcleqr  42652  limsupresre  42704  limsupresico  42708  limsuppnfdlem  42709  limsuppnflem  42718  limsupmnflem  42728  liminfresico  42779  limsup10exlem  42780  liminflelimsuplem  42783  liminflelimsupuz  42793  limsupub2  42820  liminflbuz2  42823  liminflimsupxrre  42825  xlimpnfvlem2  42845  xlimliminflimsup  42870  icccncfext  42895  iblsplit  42974  itgsubsticclem  42983  fourierdlem31  43146  fourierdlem33  43148  fourierdlem46  43160  fourierdlem47  43161  fourierdlem48  43162  fourierdlem49  43163  fourierdlem65  43179  fourierdlem73  43187  fourierdlem75  43189  fourierdlem85  43199  fourierdlem88  43202  fourierdlem95  43209  fourierdlem97  43211  fourierdlem103  43217  fourierdlem104  43218  fourierdlem107  43221  fourierdlem109  43223  fourierdlem111  43225  fourierdlem112  43226  fourierdlem113  43227  fouriersw  43239  ioorrnopnxrlem  43314  sge0val  43371  fge0iccico  43375  gsumge0cl  43376  sge0sn  43384  sge0tsms  43385  sge0cl  43386  sge0f1o  43387  sge0ge0  43389  sge0repnf  43391  sge0fsum  43392  sge0pr  43399  sge0prle  43406  sge0split  43414  sge0p1  43419  sge0iunmptlemre  43420  sge0rpcpnf  43426  sge0rernmpt  43427  sge0isum  43432  sge0ad2en  43436  sge0xaddlem1  43438  sge0xaddlem2  43439  sge0uzfsumgt  43449  sge0seq  43451  sge0reuz  43452  voliunsge0lem  43477  meage0  43480  meassre  43482  meaiuninclem  43485  omessre  43515  omeiunltfirp  43524  carageniuncllem2  43527  carageniuncl  43528  omege0  43538  hoiprodcl  43552  hoicvrrex  43561  ovnpnfelsup  43564  ovnlerp  43567  ovnf  43568  ovn0lem  43570  ovnsubaddlem1  43575  hoiprodcl3  43585  hoidmvcl  43587  sge0hsphoire  43594  hoidmv1lelem1  43596  hoidmv1lelem2  43597  hoidmv1lelem3  43598  hoidmv1le  43599  hoidmvlelem1  43600  hoidmvlelem4  43603  hoidmvlelem5  43604  ovnhoilem1  43606  volicorege0  43642  ovolval5lem1  43657  pimgtpnf2  43708  pimiooltgt  43712  smfliminflem  43827  rrxsphere  45527  itscnhlinecirc02p  45564