Theorem pnfxr 11197

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 4115	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11196	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4701	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3919	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11181	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2839	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2119   ∪ cun 3888  {cpr 4564  ℝcr 11035  +∞cpnf 11174  -∞cmnf 11175  ℝ^*cxr 11176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-un 7685  ax-cnex 11092

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-pw 4538  df-sn 4563  df-pr 4565  df-uni 4846  df-pnf 11179  df-xr 11181

This theorem is referenced by:  pnfnemnf  11198  xnn0xr  12513  xrltnr  13068  ltpnf  13069  mnfltpnf  13075  pnfnlt  13077  pnfge  13079  nltpnft  13114  xgepnf  13115  xrre  13119  xrre2  13120  xnegcl  13163  xaddf  13174  xaddpnf1  13176  xaddpnf2  13177  pnfaddmnf  13180  mnfaddpnf  13181  xaddass2  13200  xlt2add  13210  xsubge0  13211  xmulneg1  13219  xmulf  13222  xmulpnf1  13224  xmulpnf2  13225  xmulmnf1  13226  xmulpnf1n  13228  xlemul1a  13238  xadddilem  13244  xadddi2  13247  xrsupsslem  13257  xrinfmsslem  13258  supxrpnf  13268  supxrunb1  13269  supxrunb2  13270  supxrbnd  13278  xrinf0  13289  dfrp2  13345  elicore  13349  elioc2  13360  elico2  13361  elicc2  13362  ioomax  13373  iccmax  13374  ioopos  13375  elioopnf  13394  elicopnf  13396  unirnioo  13400  xrge0neqmnf  13403  elxrge0  13408  difreicc  13435  xnn0xrge0  13457  ioopnfsup  13821  icopnfsup  13822  xrsup  13825  hashbnd  14296  hashnnn0genn0  14303  hashxrcl  14317  hashdomi  14340  sgnpnf  15053  rexico  15314  limsupgre  15441  rlim3  15458  fprodge0  15956  fprodge1  15958  pcxcl  16830  pc2dvds  16848  pcadd  16858  ramxrcl  16986  ramubcl  16987  xrsnsgrp  21390  xrsdsreclblem  21395  rge0srg  21420  leordtvallem1  23200  leordtval2  23202  lecldbas  23209  pnfnei  23210  mnfnei  23211  xblpnfps  24385  xblpnf  24386  xblss2ps  24391  blssec  24425  blpnfctr  24426  nmoix  24719  icopnfcld  24757  iocmnfcld  24758  xrtgioo  24797  reconnlem1  24817  xrge0tsms  24825  metdstri  24842  iccpnfcnv  24936  ovolf  25474  ovolicopnf  25516  ovolre  25517  volsup  25548  ioombl1lem4  25553  icombl1  25555  icombl  25556  ioombl  25557  uniioombllem1  25573  mbfdm  25618  ismbfd  25631  mbfmax  25641  ismbf3d  25646  itg2ge0  25727  lhop2  26007  dvfsumlem2  26019  dvfsumrlim  26023  dvfsumrlim2  26024  taylfvallem1  26347  taylfval  26349  tayl0  26352  radcnvcl  26407  radcnvle  26410  psercnlem1  26415  logccv  26652  rlimcnp  26954  rlimcnp2  26955  xrlimcnp  26957  logfacbnd3  27211  chebbnd1  27460  chebbnd2  27465  dchrisumlem3  27479  log2sumbnd  27532  pntpbnd1  27574  pntibndlem2  27579  pntlemb  27585  pntleme  27596  pnt  27602  upgrfi  29185  topnfbey  30564  isblo3i  30897  xrge0infss  32859  xrdifh  32879  hashxpe  32906  elxrge02  33017  xdivpnfrp  33018  xrge0addass  33102  xrge0addgt0  33103  xrge0adddir  33104  xrge0npcan  33106  fsumrp0cl  33107  xrge0tsmsd  33161  pnfinf  33271  xrnarchi  33272  xrge0slmod  33438  unitssxrge0  34091  tpr2rico  34103  xrge0iifcnv  34124  xrge0iifiso  34126  xrge0iifhom  34128  xrge0mulc1cn  34132  pnfneige0  34142  lmxrge0  34143  esumle  34249  esumlef  34253  esumcst  34254  esumpr2  34258  esumpinfval  34264  esumpinfsum  34268  esumpcvgval  34269  hashf2  34275  esumcvg  34277  esumcvgsum  34279  voliune  34420  volfiniune  34421  ddemeas  34427  sxbrsigalem0  34462  sxbrsigalem2  34477  oms0  34488  sibfinima  34530  sitmcl  34542  probmeasb  34621  orvcgteel  34659  dstfrvclim1  34669  signsply0  34742  chtvalz  34820  hgt750lemf  34844  iooelexlt  37731  mbfposadd  38041  itg2addnclem2  38046  ftc1anclem5  38071  asindmre  38077  dvasin  38078  dvacos  38079  aks4d1p1p6  42565  readvrec2  42845  readvrec  42846  dvconstbi  44785  rfcnpre3  45488  absfico  45670  xadd0ge  45774  xrgepnfd  45783  xrge0nemnfd  45784  supxrgere  45785  supxrgelem  45789  supxrge  45790  xralrple2  45806  infxr  45818  infleinflem2  45822  xrralrecnnge  45841  infxrpnf  45896  xrpnf  45935  iocopn  45972  pnfel0pnf  45980  ge0xrre  45983  ge0lere  45984  ressiooinf  46009  uzinico  46011  uzubioo  46017  fsumge0cl  46025  limcicciooub  46087  limsupre  46091  limcresiooub  46092  limcleqr  46094  limsupresre  46146  limsupresico  46150  limsuppnfdlem  46151  limsuppnflem  46160  limsupmnflem  46170  liminfresico  46221  limsup10exlem  46222  liminflelimsuplem  46225  liminflelimsupuz  46235  limsupub2  46262  liminflbuz2  46265  liminflimsupxrre  46267  xlimpnfvlem2  46287  xlimliminflimsup  46312  icccncfext  46337  iblsplit  46416  itgsubsticclem  46425  fourierdlem31  46588  fourierdlem33  46590  fourierdlem46  46602  fourierdlem47  46603  fourierdlem48  46604  fourierdlem49  46605  fourierdlem65  46621  fourierdlem73  46629  fourierdlem75  46631  fourierdlem85  46641  fourierdlem88  46644  fourierdlem95  46651  fourierdlem97  46653  fourierdlem103  46659  fourierdlem104  46660  fourierdlem107  46663  fourierdlem109  46665  fourierdlem111  46667  fourierdlem112  46668  fourierdlem113  46669  fouriersw  46681  ioorrnopnxrlem  46756  sge0val  46816  fge0iccico  46820  gsumge0cl  46821  sge0sn  46829  sge0tsms  46830  sge0cl  46831  sge0f1o  46832  sge0ge0  46834  sge0repnf  46836  sge0fsum  46837  sge0pr  46844  sge0prle  46851  sge0split  46859  sge0p1  46864  sge0iunmptlemre  46865  sge0rpcpnf  46871  sge0rernmpt  46872  sge0isum  46877  sge0ad2en  46881  sge0xaddlem1  46883  sge0xaddlem2  46884  sge0uzfsumgt  46894  sge0seq  46896  sge0reuz  46897  voliunsge0lem  46922  meage0  46925  meassre  46927  meaiuninclem  46930  omessre  46960  omeiunltfirp  46969  carageniuncllem2  46972  carageniuncl  46973  omege0  46983  hoiprodcl  46997  hoicvrrex  47006  ovnpnfelsup  47009  ovnlerp  47012  ovnf  47013  ovn0lem  47015  ovnsubaddlem1  47020  hoiprodcl3  47030  hoidmvcl  47032  sge0hsphoire  47039  hoidmv1lelem1  47041  hoidmv1lelem2  47042  hoidmv1lelem3  47043  hoidmv1le  47044  hoidmvlelem1  47045  hoidmvlelem4  47048  hoidmvlelem5  47049  ovnhoilem1  47051  volicorege0  47087  ovolval5lem1  47102  pimgtpnf2f  47155  pimiooltgt  47160  smfliminflem  47280  rehalfge1  47809  rrxsphere  49246  itscnhlinecirc02p  49283