Theorem pnfxr 11198

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 4133	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11197	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4721	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3932	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11182	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2836	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2114   ∪ cun 3901  {cpr 4584  ℝcr 11037  +∞cpnf 11175  -∞cmnf 11176  ℝ^*cxr 11177

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 2709  ax-sep 5243  ax-pow 5312  ax-un 7690  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 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-pw 4558  df-sn 4583  df-pr 4585  df-uni 4866  df-pnf 11180  df-xr 11182

This theorem is referenced by:  pnfnemnf  11199  xnn0xr  12491  xrltnr  13045  ltpnf  13046  mnfltpnf  13052  pnfnlt  13054  pnfge  13056  nltpnft  13091  xgepnf  13092  xrre  13096  xrre2  13097  xnegcl  13140  xaddf  13151  xaddpnf1  13153  xaddpnf2  13154  pnfaddmnf  13157  mnfaddpnf  13158  xaddass2  13177  xlt2add  13187  xsubge0  13188  xmulneg1  13196  xmulf  13199  xmulpnf1  13201  xmulpnf2  13202  xmulmnf1  13203  xmulpnf1n  13205  xlemul1a  13215  xadddilem  13221  xadddi2  13224  xrsupsslem  13234  xrinfmsslem  13235  supxrpnf  13245  supxrunb1  13246  supxrunb2  13247  supxrbnd  13255  xrinf0  13266  dfrp2  13322  elicore  13326  elioc2  13337  elico2  13338  elicc2  13339  ioomax  13350  iccmax  13351  ioopos  13352  elioopnf  13371  elicopnf  13373  unirnioo  13377  xrge0neqmnf  13380  elxrge0  13385  difreicc  13412  xnn0xrge0  13434  ioopnfsup  13796  icopnfsup  13797  xrsup  13800  hashbnd  14271  hashnnn0genn0  14278  hashxrcl  14292  hashdomi  14315  sgnpnf  15028  rexico  15289  limsupgre  15416  rlim3  15433  fprodge0  15928  fprodge1  15930  pcxcl  16801  pc2dvds  16819  pcadd  16829  ramxrcl  16957  ramubcl  16958  xrsnsgrp  21374  xrsdsreclblem  21379  rge0srg  21405  leordtvallem1  23166  leordtval2  23168  lecldbas  23175  pnfnei  23176  mnfnei  23177  xblpnfps  24351  xblpnf  24352  xblss2ps  24357  blssec  24391  blpnfctr  24392  nmoix  24685  icopnfcld  24723  iocmnfcld  24724  xrtgioo  24763  reconnlem1  24783  xrge0tsms  24791  metdstri  24808  iccpnfcnv  24910  ovolf  25451  ovolicopnf  25493  ovolre  25494  volsup  25525  ioombl1lem4  25530  icombl1  25532  icombl  25533  ioombl  25534  uniioombllem1  25550  mbfdm  25595  ismbfd  25608  mbfmax  25618  ismbf3d  25623  itg2ge0  25704  lhop2  25988  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumrlim  26006  dvfsumrlim2  26007  taylfvallem1  26332  taylfval  26334  tayl0  26337  radcnvcl  26394  radcnvle  26397  psercnlem1  26403  logccv  26640  rlimcnp  26943  rlimcnp2  26944  xrlimcnp  26946  logfacbnd3  27202  chebbnd1  27451  chebbnd2  27456  dchrisumlem3  27470  log2sumbnd  27523  pntpbnd1  27565  pntibndlem2  27570  pntlemb  27576  pntleme  27587  pnt  27593  upgrfi  29176  topnfbey  30556  isblo3i  30888  xrge0infss  32850  xrdifh  32870  hashxpe  32897  elxrge02  33023  xdivpnfrp  33024  xrge0addass  33108  xrge0addgt0  33109  xrge0adddir  33110  xrge0npcan  33112  fsumrp0cl  33113  xrge0tsmsd  33166  pnfinf  33276  xrnarchi  33277  xrge0slmod  33440  unitssxrge0  34077  tpr2rico  34089  xrge0iifcnv  34110  xrge0iifiso  34112  xrge0iifhom  34114  xrge0mulc1cn  34118  pnfneige0  34128  lmxrge0  34129  esumle  34235  esumlef  34239  esumcst  34240  esumpr2  34244  esumpinfval  34250  esumpinfsum  34254  esumpcvgval  34255  hashf2  34261  esumcvg  34263  esumcvgsum  34265  voliune  34406  volfiniune  34407  ddemeas  34413  sxbrsigalem0  34448  sxbrsigalem2  34463  oms0  34474  sibfinima  34516  sitmcl  34528  probmeasb  34607  orvcgteel  34645  dstfrvclim1  34655  signsply0  34728  chtvalz  34806  hgt750lemf  34830  iooelexlt  37611  mbfposadd  37912  itg2addnclem2  37917  ftc1anclem5  37942  asindmre  37948  dvasin  37949  dvacos  37950  aks4d1p1p6  42437  readvrec2  42725  readvrec  42726  dvconstbi  44684  rfcnpre3  45387  absfico  45570  xadd0ge  45675  xrgepnfd  45684  xrge0nemnfd  45685  supxrgere  45686  supxrgelem  45690  supxrge  45691  xralrple2  45707  infxr  45719  infleinflem2  45723  xrralrecnnge  45742  infxrpnf  45798  xrpnf  45837  iocopn  45874  pnfel0pnf  45882  ge0xrre  45885  ge0lere  45886  ressiooinf  45911  uzinico  45913  uzubioo  45919  fsumge0cl  45927  limcicciooub  45989  limsupre  45993  limcresiooub  45994  limcleqr  45996  limsupresre  46048  limsupresico  46052  limsuppnfdlem  46053  limsuppnflem  46062  limsupmnflem  46072  liminfresico  46123  limsup10exlem  46124  liminflelimsuplem  46127  liminflelimsupuz  46137  limsupub2  46164  liminflbuz2  46167  liminflimsupxrre  46169  xlimpnfvlem2  46189  xlimliminflimsup  46214  icccncfext  46239  iblsplit  46318  itgsubsticclem  46327  fourierdlem31  46490  fourierdlem33  46492  fourierdlem46  46504  fourierdlem47  46505  fourierdlem48  46506  fourierdlem49  46507  fourierdlem65  46523  fourierdlem73  46531  fourierdlem75  46533  fourierdlem85  46543  fourierdlem88  46546  fourierdlem95  46553  fourierdlem97  46555  fourierdlem103  46561  fourierdlem104  46562  fourierdlem107  46565  fourierdlem109  46567  fourierdlem111  46569  fourierdlem112  46570  fourierdlem113  46571  fouriersw  46583  ioorrnopnxrlem  46658  sge0val  46718  fge0iccico  46722  gsumge0cl  46723  sge0sn  46731  sge0tsms  46732  sge0cl  46733  sge0f1o  46734  sge0ge0  46736  sge0repnf  46738  sge0fsum  46739  sge0pr  46746  sge0prle  46753  sge0split  46761  sge0p1  46766  sge0iunmptlemre  46767  sge0rpcpnf  46773  sge0rernmpt  46774  sge0isum  46779  sge0ad2en  46783  sge0xaddlem1  46785  sge0xaddlem2  46786  sge0uzfsumgt  46796  sge0seq  46798  sge0reuz  46799  voliunsge0lem  46824  meage0  46827  meassre  46829  meaiuninclem  46832  omessre  46862  omeiunltfirp  46871  carageniuncllem2  46874  carageniuncl  46875  omege0  46885  hoiprodcl  46899  hoicvrrex  46908  ovnpnfelsup  46911  ovnlerp  46914  ovnf  46915  ovn0lem  46917  ovnsubaddlem1  46922  hoiprodcl3  46932  hoidmvcl  46934  sge0hsphoire  46941  hoidmv1lelem1  46943  hoidmv1lelem2  46944  hoidmv1lelem3  46945  hoidmv1le  46946  hoidmvlelem1  46947  hoidmvlelem4  46950  hoidmvlelem5  46951  ovnhoilem1  46953  volicorege0  46989  ovolval5lem1  47004  pimgtpnf2f  47057  pimiooltgt  47062  smfliminflem  47182  rehalfge1  47689  rrxsphere  49102  itscnhlinecirc02p  49139