Theorem pnfxr 11163

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 4129	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11162	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4715	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3931	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11147	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2830	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2111   ∪ cun 3900  {cpr 4578  ℝcr 11002  +∞cpnf 11140  -∞cmnf 11141  ℝ^*cxr 11142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-pow 5303  ax-un 7668  ax-cnex 11059

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919  df-pw 4552  df-sn 4577  df-pr 4579  df-uni 4860  df-pnf 11145  df-xr 11147

This theorem is referenced by:  pnfnemnf  11164  xnn0xr  12456  xrltnr  13015  ltpnf  13016  mnfltpnf  13022  pnfnlt  13024  pnfge  13026  nltpnft  13060  xgepnf  13061  xrre  13065  xrre2  13066  xnegcl  13109  xaddf  13120  xaddpnf1  13122  xaddpnf2  13123  pnfaddmnf  13126  mnfaddpnf  13127  xaddass2  13146  xlt2add  13156  xsubge0  13157  xmulneg1  13165  xmulf  13168  xmulpnf1  13170  xmulpnf2  13171  xmulmnf1  13172  xmulpnf1n  13174  xlemul1a  13184  xadddilem  13190  xadddi2  13193  xrsupsslem  13203  xrinfmsslem  13204  supxrpnf  13214  supxrunb1  13215  supxrunb2  13216  supxrbnd  13224  xrinf0  13235  dfrp2  13291  elicore  13295  elioc2  13306  elico2  13307  elicc2  13308  ioomax  13319  iccmax  13320  ioopos  13321  elioopnf  13340  elicopnf  13342  unirnioo  13346  xrge0neqmnf  13349  elxrge0  13354  difreicc  13381  xnn0xrge0  13403  ioopnfsup  13765  icopnfsup  13766  xrsup  13769  hashbnd  14240  hashnnn0genn0  14247  hashxrcl  14261  hashdomi  14284  sgnpnf  14997  rexico  15258  limsupgre  15385  rlim3  15402  fprodge0  15897  fprodge1  15899  pcxcl  16770  pc2dvds  16788  pcadd  16798  ramxrcl  16926  ramubcl  16927  xrsnsgrp  21342  xrsdsreclblem  21347  rge0srg  21373  leordtvallem1  23123  leordtval2  23125  lecldbas  23132  pnfnei  23133  mnfnei  23134  xblpnfps  24308  xblpnf  24309  xblss2ps  24314  blssec  24348  blpnfctr  24349  nmoix  24642  icopnfcld  24680  iocmnfcld  24681  xrtgioo  24720  reconnlem1  24740  xrge0tsms  24748  metdstri  24765  iccpnfcnv  24867  ovolf  25408  ovolicopnf  25450  ovolre  25451  volsup  25482  ioombl1lem4  25487  icombl1  25489  icombl  25490  ioombl  25491  uniioombllem1  25507  mbfdm  25552  ismbfd  25565  mbfmax  25575  ismbf3d  25580  itg2ge0  25661  lhop2  25945  dvfsumlem2  25958  dvfsumlem2OLD  25959  dvfsumrlim  25963  dvfsumrlim2  25964  taylfvallem1  26289  taylfval  26291  tayl0  26294  radcnvcl  26351  radcnvle  26354  psercnlem1  26360  logccv  26597  rlimcnp  26900  rlimcnp2  26901  xrlimcnp  26903  logfacbnd3  27159  chebbnd1  27408  chebbnd2  27413  dchrisumlem3  27427  log2sumbnd  27480  pntpbnd1  27522  pntibndlem2  27527  pntlemb  27533  pntleme  27544  pnt  27550  upgrfi  29067  topnfbey  30444  isblo3i  30776  xrge0infss  32738  xrdifh  32758  hashxpe  32784  elxrge02  32907  xdivpnfrp  32908  xrge0addass  32992  xrge0addgt0  32993  xrge0adddir  32994  xrge0npcan  32996  fsumrp0cl  32997  xrge0tsmsd  33037  pnfinf  33147  xrnarchi  33148  xrge0slmod  33308  unitssxrge0  33908  tpr2rico  33920  xrge0iifcnv  33941  xrge0iifiso  33943  xrge0iifhom  33945  xrge0mulc1cn  33949  pnfneige0  33959  lmxrge0  33960  esumle  34066  esumlef  34070  esumcst  34071  esumpr2  34075  esumpinfval  34081  esumpinfsum  34085  esumpcvgval  34086  hashf2  34092  esumcvg  34094  esumcvgsum  34096  voliune  34237  volfiniune  34238  ddemeas  34244  sxbrsigalem0  34279  sxbrsigalem2  34294  oms0  34305  sibfinima  34347  sitmcl  34359  probmeasb  34438  orvcgteel  34476  dstfrvclim1  34486  signsply0  34559  chtvalz  34637  hgt750lemf  34661  iooelexlt  37395  mbfposadd  37706  itg2addnclem2  37711  ftc1anclem5  37736  asindmre  37742  dvasin  37743  dvacos  37744  aks4d1p1p6  42105  readvrec2  42393  readvrec  42394  dvconstbi  44366  rfcnpre3  45069  absfico  45254  xadd0ge  45359  xrgepnfd  45369  xrge0nemnfd  45370  supxrgere  45371  supxrgelem  45375  supxrge  45376  xralrple2  45392  infxr  45404  infleinflem2  45408  xrralrecnnge  45427  infxrpnf  45483  xrpnf  45522  iocopn  45559  pnfel0pnf  45567  ge0xrre  45570  ge0lere  45571  ressiooinf  45596  uzinico  45598  uzubioo  45604  fsumge0cl  45612  limcicciooub  45674  limsupre  45678  limcresiooub  45679  limcleqr  45681  limsupresre  45733  limsupresico  45737  limsuppnfdlem  45738  limsuppnflem  45747  limsupmnflem  45757  liminfresico  45808  limsup10exlem  45809  liminflelimsuplem  45812  liminflelimsupuz  45822  limsupub2  45849  liminflbuz2  45852  liminflimsupxrre  45854  xlimpnfvlem2  45874  xlimliminflimsup  45899  icccncfext  45924  iblsplit  46003  itgsubsticclem  46012  fourierdlem31  46175  fourierdlem33  46177  fourierdlem46  46189  fourierdlem47  46190  fourierdlem48  46191  fourierdlem49  46192  fourierdlem65  46208  fourierdlem73  46216  fourierdlem75  46218  fourierdlem85  46228  fourierdlem88  46231  fourierdlem95  46238  fourierdlem97  46240  fourierdlem103  46246  fourierdlem104  46247  fourierdlem107  46250  fourierdlem109  46252  fourierdlem111  46254  fourierdlem112  46255  fourierdlem113  46256  fouriersw  46268  ioorrnopnxrlem  46343  sge0val  46403  fge0iccico  46407  gsumge0cl  46408  sge0sn  46416  sge0tsms  46417  sge0cl  46418  sge0f1o  46419  sge0ge0  46421  sge0repnf  46423  sge0fsum  46424  sge0pr  46431  sge0prle  46438  sge0split  46446  sge0p1  46451  sge0iunmptlemre  46452  sge0rpcpnf  46458  sge0rernmpt  46459  sge0isum  46464  sge0ad2en  46468  sge0xaddlem1  46470  sge0xaddlem2  46471  sge0uzfsumgt  46481  sge0seq  46483  sge0reuz  46484  voliunsge0lem  46509  meage0  46512  meassre  46514  meaiuninclem  46517  omessre  46547  omeiunltfirp  46556  carageniuncllem2  46559  carageniuncl  46560  omege0  46570  hoiprodcl  46584  hoicvrrex  46593  ovnpnfelsup  46596  ovnlerp  46599  ovnf  46600  ovn0lem  46602  ovnsubaddlem1  46607  hoiprodcl3  46617  hoidmvcl  46619  sge0hsphoire  46626  hoidmv1lelem1  46628  hoidmv1lelem2  46629  hoidmv1lelem3  46630  hoidmv1le  46631  hoidmvlelem1  46632  hoidmvlelem4  46635  hoidmvlelem5  46636  ovnhoilem1  46638  volicorege0  46674  ovolval5lem1  46689  pimgtpnf2f  46742  pimiooltgt  46747  smfliminflem  46867  rehalfge1  47365  rrxsphere  48779  itscnhlinecirc02p  48816