Theorem pnfxr 11255

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 4171	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11254	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4762	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3977	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11239	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2833	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2107   ∪ cun 3944  {cpr 4626  ℝcr 11096  +∞cpnf 11232  -∞cmnf 11233  ℝ^*cxr 11234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5295  ax-pow 5359  ax-un 7712  ax-cnex 11153

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3951  df-in 3953  df-ss 3963  df-pw 4600  df-sn 4625  df-pr 4627  df-uni 4905  df-pnf 11237  df-xr 11239

This theorem is referenced by:  pnfnemnf  11256  xnn0xr  12536  xrltnr  13086  ltpnf  13087  mnfltpnf  13093  pnfnlt  13095  pnfge  13097  nltpnft  13130  xgepnf  13131  xrre  13135  xrre2  13136  xnegcl  13179  xaddf  13190  xaddpnf1  13192  xaddpnf2  13193  pnfaddmnf  13196  mnfaddpnf  13197  xaddass2  13216  xlt2add  13226  xsubge0  13227  xmulneg1  13235  xmulf  13238  xmulpnf1  13240  xmulpnf2  13241  xmulmnf1  13242  xmulpnf1n  13244  xlemul1a  13254  xadddilem  13260  xadddi2  13263  xrsupsslem  13273  xrinfmsslem  13274  supxrpnf  13284  supxrunb1  13285  supxrunb2  13286  supxrbnd  13294  xrinf0  13304  dfrp2  13360  elicore  13363  elioc2  13374  elico2  13375  elicc2  13376  ioomax  13386  iccmax  13387  ioopos  13388  elioopnf  13407  elicopnf  13409  unirnioo  13413  xrge0neqmnf  13416  elxrge0  13421  difreicc  13448  xnn0xrge0  13470  ioopnfsup  13816  icopnfsup  13817  xrsup  13820  hashbnd  14283  hashnnn0genn0  14290  hashxrcl  14304  hashdomi  14327  sgnpnf  15027  rexico  15287  limsupgre  15412  rlim3  15429  fprodge0  15924  fprodge1  15926  pcxcl  16781  pc2dvds  16799  pcadd  16809  ramxrcl  16937  ramubcl  16938  xrsnsgrp  20955  xrsdsreclblem  20965  rge0srg  20990  leordtvallem1  22683  leordtval2  22685  lecldbas  22692  pnfnei  22693  mnfnei  22694  xblpnfps  23870  xblpnf  23871  xblss2ps  23876  blssec  23910  blpnfctr  23911  nmoix  24215  icopnfcld  24253  iocmnfcld  24254  xrtgioo  24291  reconnlem1  24311  xrge0tsms  24319  metdstri  24336  iccpnfcnv  24429  ovolf  24968  ovolicopnf  25010  ovolre  25011  volsup  25042  ioombl1lem4  25047  icombl1  25049  icombl  25050  ioombl  25051  uniioombllem1  25067  mbfdm  25112  ismbfd  25125  mbfmax  25135  ismbf3d  25140  itg2ge0  25222  lhop2  25501  dvfsumlem2  25513  dvfsumrlim  25517  dvfsumrlim2  25518  taylfvallem1  25838  taylfval  25840  tayl0  25843  radcnvcl  25898  radcnvle  25901  psercnlem1  25906  logccv  26140  rlimcnp  26437  rlimcnp2  26438  xrlimcnp  26440  logfacbnd3  26693  chebbnd1  26942  chebbnd2  26947  dchrisumlem3  26961  log2sumbnd  27014  pntpbnd1  27056  pntibndlem2  27061  pntlemb  27067  pntleme  27078  pnt  27084  upgrfi  28318  topnfbey  29689  isblo3i  30019  xrge0infss  31944  xrdifh  31962  hashxpe  31990  elxrge02  32069  xdivpnfrp  32070  xrge0addass  32162  xrge0addgt0  32163  xrge0adddir  32164  xrge0npcan  32166  fsumrp0cl  32167  xrge0tsmsd  32180  pnfinf  32300  xrnarchi  32301  xrge0slmod  32425  unitssxrge0  32811  tpr2rico  32823  xrge0iifcnv  32844  xrge0iifiso  32846  xrge0iifhom  32848  xrge0mulc1cn  32852  pnfneige0  32862  lmxrge0  32863  esumle  32987  esumlef  32991  esumcst  32992  esumpr2  32996  esumpinfval  33002  esumpinfsum  33006  esumpcvgval  33007  hashf2  33013  esumcvg  33015  esumcvgsum  33017  voliune  33158  volfiniune  33159  ddemeas  33165  sxbrsigalem0  33201  sxbrsigalem2  33216  oms0  33227  sibfinima  33269  sitmcl  33281  probmeasb  33360  orvcgteel  33397  dstfrvclim1  33407  signsply0  33493  chtvalz  33572  hgt750lemf  33596  iooelexlt  36148  mbfposadd  36440  itg2addnclem2  36445  ftc1anclem5  36470  asindmre  36476  dvasin  36477  dvacos  36478  aks4d1p1p6  40844  dvconstbi  42964  rfcnpre3  43588  absfico  43788  xadd0ge  43903  xrgepnfd  43914  xrge0nemnfd  43915  supxrgere  43916  supxrgelem  43920  supxrge  43921  xralrple2  43937  infxr  43950  infleinflem2  43954  xrralrecnnge  43973  infxrpnf  44029  xrpnf  44069  iocopn  44106  pnfel0pnf  44114  ge0xrre  44117  ge0lere  44118  ressiooinf  44143  uzinico  44146  uzubioo  44153  fsumge0cl  44162  limcicciooub  44226  limsupre  44230  limcresiooub  44231  limcleqr  44233  limsupresre  44285  limsupresico  44289  limsuppnfdlem  44290  limsuppnflem  44299  limsupmnflem  44309  liminfresico  44360  limsup10exlem  44361  liminflelimsuplem  44364  liminflelimsupuz  44374  limsupub2  44401  liminflbuz2  44404  liminflimsupxrre  44406  xlimpnfvlem2  44426  xlimliminflimsup  44451  icccncfext  44476  iblsplit  44555  itgsubsticclem  44564  fourierdlem31  44727  fourierdlem33  44729  fourierdlem46  44741  fourierdlem47  44742  fourierdlem48  44743  fourierdlem49  44744  fourierdlem65  44760  fourierdlem73  44768  fourierdlem75  44770  fourierdlem85  44780  fourierdlem88  44783  fourierdlem95  44790  fourierdlem97  44792  fourierdlem103  44798  fourierdlem104  44799  fourierdlem107  44802  fourierdlem109  44804  fourierdlem111  44806  fourierdlem112  44807  fourierdlem113  44808  fouriersw  44820  ioorrnopnxrlem  44895  sge0val  44955  fge0iccico  44959  gsumge0cl  44960  sge0sn  44968  sge0tsms  44969  sge0cl  44970  sge0f1o  44971  sge0ge0  44973  sge0repnf  44975  sge0fsum  44976  sge0pr  44983  sge0prle  44990  sge0split  44998  sge0p1  45003  sge0iunmptlemre  45004  sge0rpcpnf  45010  sge0rernmpt  45011  sge0isum  45016  sge0ad2en  45020  sge0xaddlem1  45022  sge0xaddlem2  45023  sge0uzfsumgt  45033  sge0seq  45035  sge0reuz  45036  voliunsge0lem  45061  meage0  45064  meassre  45066  meaiuninclem  45069  omessre  45099  omeiunltfirp  45108  carageniuncllem2  45111  carageniuncl  45112  omege0  45122  hoiprodcl  45136  hoicvrrex  45145  ovnpnfelsup  45148  ovnlerp  45151  ovnf  45152  ovn0lem  45154  ovnsubaddlem1  45159  hoiprodcl3  45169  hoidmvcl  45171  sge0hsphoire  45178  hoidmv1lelem1  45180  hoidmv1lelem2  45181  hoidmv1lelem3  45182  hoidmv1le  45183  hoidmvlelem1  45184  hoidmvlelem4  45187  hoidmvlelem5  45188  ovnhoilem1  45190  volicorege0  45226  ovolval5lem1  45241  pimgtpnf2f  45294  pimiooltgt  45299  smfliminflem  45419  rrxsphere  47274  itscnhlinecirc02p  47311