Theorem pnfxr 11186

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 4131	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11185	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4719	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3930	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11170	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2835	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2113   ∪ cun 3899  {cpr 4582  ℝcr 11025  +∞cpnf 11163  -∞cmnf 11164  ℝ^*cxr 11165

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-pow 5310  ax-un 7680  ax-cnex 11082

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-pw 4556  df-sn 4581  df-pr 4583  df-uni 4864  df-pnf 11168  df-xr 11170

This theorem is referenced by:  pnfnemnf  11187  xnn0xr  12479  xrltnr  13033  ltpnf  13034  mnfltpnf  13040  pnfnlt  13042  pnfge  13044  nltpnft  13079  xgepnf  13080  xrre  13084  xrre2  13085  xnegcl  13128  xaddf  13139  xaddpnf1  13141  xaddpnf2  13142  pnfaddmnf  13145  mnfaddpnf  13146  xaddass2  13165  xlt2add  13175  xsubge0  13176  xmulneg1  13184  xmulf  13187  xmulpnf1  13189  xmulpnf2  13190  xmulmnf1  13191  xmulpnf1n  13193  xlemul1a  13203  xadddilem  13209  xadddi2  13212  xrsupsslem  13222  xrinfmsslem  13223  supxrpnf  13233  supxrunb1  13234  supxrunb2  13235  supxrbnd  13243  xrinf0  13254  dfrp2  13310  elicore  13314  elioc2  13325  elico2  13326  elicc2  13327  ioomax  13338  iccmax  13339  ioopos  13340  elioopnf  13359  elicopnf  13361  unirnioo  13365  xrge0neqmnf  13368  elxrge0  13373  difreicc  13400  xnn0xrge0  13422  ioopnfsup  13784  icopnfsup  13785  xrsup  13788  hashbnd  14259  hashnnn0genn0  14266  hashxrcl  14280  hashdomi  14303  sgnpnf  15016  rexico  15277  limsupgre  15404  rlim3  15421  fprodge0  15916  fprodge1  15918  pcxcl  16789  pc2dvds  16807  pcadd  16817  ramxrcl  16945  ramubcl  16946  xrsnsgrp  21362  xrsdsreclblem  21367  rge0srg  21393  leordtvallem1  23154  leordtval2  23156  lecldbas  23163  pnfnei  23164  mnfnei  23165  xblpnfps  24339  xblpnf  24340  xblss2ps  24345  blssec  24379  blpnfctr  24380  nmoix  24673  icopnfcld  24711  iocmnfcld  24712  xrtgioo  24751  reconnlem1  24771  xrge0tsms  24779  metdstri  24796  iccpnfcnv  24898  ovolf  25439  ovolicopnf  25481  ovolre  25482  volsup  25513  ioombl1lem4  25518  icombl1  25520  icombl  25521  ioombl  25522  uniioombllem1  25538  mbfdm  25583  ismbfd  25596  mbfmax  25606  ismbf3d  25611  itg2ge0  25692  lhop2  25976  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumrlim  25994  dvfsumrlim2  25995  taylfvallem1  26320  taylfval  26322  tayl0  26325  radcnvcl  26382  radcnvle  26385  psercnlem1  26391  logccv  26628  rlimcnp  26931  rlimcnp2  26932  xrlimcnp  26934  logfacbnd3  27190  chebbnd1  27439  chebbnd2  27444  dchrisumlem3  27458  log2sumbnd  27511  pntpbnd1  27553  pntibndlem2  27558  pntlemb  27564  pntleme  27575  pnt  27581  upgrfi  29164  topnfbey  30544  isblo3i  30876  xrge0infss  32840  xrdifh  32860  hashxpe  32887  elxrge02  33013  xdivpnfrp  33014  xrge0addass  33098  xrge0addgt0  33099  xrge0adddir  33100  xrge0npcan  33102  fsumrp0cl  33103  xrge0tsmsd  33155  pnfinf  33265  xrnarchi  33266  xrge0slmod  33429  unitssxrge0  34057  tpr2rico  34069  xrge0iifcnv  34090  xrge0iifiso  34092  xrge0iifhom  34094  xrge0mulc1cn  34098  pnfneige0  34108  lmxrge0  34109  esumle  34215  esumlef  34219  esumcst  34220  esumpr2  34224  esumpinfval  34230  esumpinfsum  34234  esumpcvgval  34235  hashf2  34241  esumcvg  34243  esumcvgsum  34245  voliune  34386  volfiniune  34387  ddemeas  34393  sxbrsigalem0  34428  sxbrsigalem2  34443  oms0  34454  sibfinima  34496  sitmcl  34508  probmeasb  34587  orvcgteel  34625  dstfrvclim1  34635  signsply0  34708  chtvalz  34786  hgt750lemf  34810  iooelexlt  37563  mbfposadd  37864  itg2addnclem2  37869  ftc1anclem5  37894  asindmre  37900  dvasin  37901  dvacos  37902  aks4d1p1p6  42323  readvrec2  42612  readvrec  42613  dvconstbi  44571  rfcnpre3  45274  absfico  45458  xadd0ge  45563  xrgepnfd  45572  xrge0nemnfd  45573  supxrgere  45574  supxrgelem  45578  supxrge  45579  xralrple2  45595  infxr  45607  infleinflem2  45611  xrralrecnnge  45630  infxrpnf  45686  xrpnf  45725  iocopn  45762  pnfel0pnf  45770  ge0xrre  45773  ge0lere  45774  ressiooinf  45799  uzinico  45801  uzubioo  45807  fsumge0cl  45815  limcicciooub  45877  limsupre  45881  limcresiooub  45882  limcleqr  45884  limsupresre  45936  limsupresico  45940  limsuppnfdlem  45941  limsuppnflem  45950  limsupmnflem  45960  liminfresico  46011  limsup10exlem  46012  liminflelimsuplem  46015  liminflelimsupuz  46025  limsupub2  46052  liminflbuz2  46055  liminflimsupxrre  46057  xlimpnfvlem2  46077  xlimliminflimsup  46102  icccncfext  46127  iblsplit  46206  itgsubsticclem  46215  fourierdlem31  46378  fourierdlem33  46380  fourierdlem46  46392  fourierdlem47  46393  fourierdlem48  46394  fourierdlem49  46395  fourierdlem65  46411  fourierdlem73  46419  fourierdlem75  46421  fourierdlem85  46431  fourierdlem88  46434  fourierdlem95  46441  fourierdlem97  46443  fourierdlem103  46449  fourierdlem104  46450  fourierdlem107  46453  fourierdlem109  46455  fourierdlem111  46457  fourierdlem112  46458  fourierdlem113  46459  fouriersw  46471  ioorrnopnxrlem  46546  sge0val  46606  fge0iccico  46610  gsumge0cl  46611  sge0sn  46619  sge0tsms  46620  sge0cl  46621  sge0f1o  46622  sge0ge0  46624  sge0repnf  46626  sge0fsum  46627  sge0pr  46634  sge0prle  46641  sge0split  46649  sge0p1  46654  sge0iunmptlemre  46655  sge0rpcpnf  46661  sge0rernmpt  46662  sge0isum  46667  sge0ad2en  46671  sge0xaddlem1  46673  sge0xaddlem2  46674  sge0uzfsumgt  46684  sge0seq  46686  sge0reuz  46687  voliunsge0lem  46712  meage0  46715  meassre  46717  meaiuninclem  46720  omessre  46750  omeiunltfirp  46759  carageniuncllem2  46762  carageniuncl  46763  omege0  46773  hoiprodcl  46787  hoicvrrex  46796  ovnpnfelsup  46799  ovnlerp  46802  ovnf  46803  ovn0lem  46805  ovnsubaddlem1  46810  hoiprodcl3  46820  hoidmvcl  46822  sge0hsphoire  46829  hoidmv1lelem1  46831  hoidmv1lelem2  46832  hoidmv1lelem3  46833  hoidmv1le  46834  hoidmvlelem1  46835  hoidmvlelem4  46838  hoidmvlelem5  46839  ovnhoilem1  46841  volicorege0  46877  ovolval5lem1  46892  pimgtpnf2f  46945  pimiooltgt  46950  smfliminflem  47070  rehalfge1  47577  rrxsphere  48990  itscnhlinecirc02p  49027