Theorem pnfxr 11315

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 4179	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11314	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4762	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3980	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11299	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2840	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2108   ∪ cun 3949  {cpr 4628  ℝcr 11154  +∞cpnf 11292  -∞cmnf 11293  ℝ^*cxr 11294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-pow 5365  ax-un 7755  ax-cnex 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-pw 4602  df-sn 4627  df-pr 4629  df-uni 4908  df-pnf 11297  df-xr 11299

This theorem is referenced by:  pnfnemnf  11316  xnn0xr  12604  xrltnr  13161  ltpnf  13162  mnfltpnf  13168  pnfnlt  13170  pnfge  13172  nltpnft  13206  xgepnf  13207  xrre  13211  xrre2  13212  xnegcl  13255  xaddf  13266  xaddpnf1  13268  xaddpnf2  13269  pnfaddmnf  13272  mnfaddpnf  13273  xaddass2  13292  xlt2add  13302  xsubge0  13303  xmulneg1  13311  xmulf  13314  xmulpnf1  13316  xmulpnf2  13317  xmulmnf1  13318  xmulpnf1n  13320  xlemul1a  13330  xadddilem  13336  xadddi2  13339  xrsupsslem  13349  xrinfmsslem  13350  supxrpnf  13360  supxrunb1  13361  supxrunb2  13362  supxrbnd  13370  xrinf0  13380  dfrp2  13436  elicore  13439  elioc2  13450  elico2  13451  elicc2  13452  ioomax  13462  iccmax  13463  ioopos  13464  elioopnf  13483  elicopnf  13485  unirnioo  13489  xrge0neqmnf  13492  elxrge0  13497  difreicc  13524  xnn0xrge0  13546  ioopnfsup  13904  icopnfsup  13905  xrsup  13908  hashbnd  14375  hashnnn0genn0  14382  hashxrcl  14396  hashdomi  14419  sgnpnf  15132  rexico  15392  limsupgre  15517  rlim3  15534  fprodge0  16029  fprodge1  16031  pcxcl  16899  pc2dvds  16917  pcadd  16927  ramxrcl  17055  ramubcl  17056  xrsnsgrp  21420  xrsdsreclblem  21430  rge0srg  21456  leordtvallem1  23218  leordtval2  23220  lecldbas  23227  pnfnei  23228  mnfnei  23229  xblpnfps  24405  xblpnf  24406  xblss2ps  24411  blssec  24445  blpnfctr  24446  nmoix  24750  icopnfcld  24788  iocmnfcld  24789  xrtgioo  24828  reconnlem1  24848  xrge0tsms  24856  metdstri  24873  iccpnfcnv  24975  ovolf  25517  ovolicopnf  25559  ovolre  25560  volsup  25591  ioombl1lem4  25596  icombl1  25598  icombl  25599  ioombl  25600  uniioombllem1  25616  mbfdm  25661  ismbfd  25674  mbfmax  25684  ismbf3d  25689  itg2ge0  25770  lhop2  26054  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumrlim  26072  dvfsumrlim2  26073  taylfvallem1  26398  taylfval  26400  tayl0  26403  radcnvcl  26460  radcnvle  26463  psercnlem1  26469  logccv  26705  rlimcnp  27008  rlimcnp2  27009  xrlimcnp  27011  logfacbnd3  27267  chebbnd1  27516  chebbnd2  27521  dchrisumlem3  27535  log2sumbnd  27588  pntpbnd1  27630  pntibndlem2  27635  pntlemb  27641  pntleme  27652  pnt  27658  upgrfi  29108  topnfbey  30488  isblo3i  30820  xrge0infss  32764  xrdifh  32782  hashxpe  32811  elxrge02  32914  xdivpnfrp  32915  xrge0addass  33021  xrge0addgt0  33022  xrge0adddir  33023  xrge0npcan  33025  fsumrp0cl  33026  xrge0tsmsd  33065  pnfinf  33190  xrnarchi  33191  xrge0slmod  33376  unitssxrge0  33899  tpr2rico  33911  xrge0iifcnv  33932  xrge0iifiso  33934  xrge0iifhom  33936  xrge0mulc1cn  33940  pnfneige0  33950  lmxrge0  33951  esumle  34059  esumlef  34063  esumcst  34064  esumpr2  34068  esumpinfval  34074  esumpinfsum  34078  esumpcvgval  34079  hashf2  34085  esumcvg  34087  esumcvgsum  34089  voliune  34230  volfiniune  34231  ddemeas  34237  sxbrsigalem0  34273  sxbrsigalem2  34288  oms0  34299  sibfinima  34341  sitmcl  34353  probmeasb  34432  orvcgteel  34470  dstfrvclim1  34480  signsply0  34566  chtvalz  34644  hgt750lemf  34668  iooelexlt  37363  mbfposadd  37674  itg2addnclem2  37679  ftc1anclem5  37704  asindmre  37710  dvasin  37711  dvacos  37712  aks4d1p1p6  42074  readvrec2  42391  readvrec  42392  dvconstbi  44353  rfcnpre3  45038  absfico  45223  xadd0ge  45332  xrgepnfd  45342  xrge0nemnfd  45343  supxrgere  45344  supxrgelem  45348  supxrge  45349  xralrple2  45365  infxr  45378  infleinflem2  45382  xrralrecnnge  45401  infxrpnf  45457  xrpnf  45496  iocopn  45533  pnfel0pnf  45541  ge0xrre  45544  ge0lere  45545  ressiooinf  45570  uzinico  45573  uzubioo  45580  fsumge0cl  45588  limcicciooub  45652  limsupre  45656  limcresiooub  45657  limcleqr  45659  limsupresre  45711  limsupresico  45715  limsuppnfdlem  45716  limsuppnflem  45725  limsupmnflem  45735  liminfresico  45786  limsup10exlem  45787  liminflelimsuplem  45790  liminflelimsupuz  45800  limsupub2  45827  liminflbuz2  45830  liminflimsupxrre  45832  xlimpnfvlem2  45852  xlimliminflimsup  45877  icccncfext  45902  iblsplit  45981  itgsubsticclem  45990  fourierdlem31  46153  fourierdlem33  46155  fourierdlem46  46167  fourierdlem47  46168  fourierdlem48  46169  fourierdlem49  46170  fourierdlem65  46186  fourierdlem73  46194  fourierdlem75  46196  fourierdlem85  46206  fourierdlem88  46209  fourierdlem95  46216  fourierdlem97  46218  fourierdlem103  46224  fourierdlem104  46225  fourierdlem107  46228  fourierdlem109  46230  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  fouriersw  46246  ioorrnopnxrlem  46321  sge0val  46381  fge0iccico  46385  gsumge0cl  46386  sge0sn  46394  sge0tsms  46395  sge0cl  46396  sge0f1o  46397  sge0ge0  46399  sge0repnf  46401  sge0fsum  46402  sge0pr  46409  sge0prle  46416  sge0split  46424  sge0p1  46429  sge0iunmptlemre  46430  sge0rpcpnf  46436  sge0rernmpt  46437  sge0isum  46442  sge0ad2en  46446  sge0xaddlem1  46448  sge0xaddlem2  46449  sge0uzfsumgt  46459  sge0seq  46461  sge0reuz  46462  voliunsge0lem  46487  meage0  46490  meassre  46492  meaiuninclem  46495  omessre  46525  omeiunltfirp  46534  carageniuncllem2  46537  carageniuncl  46538  omege0  46548  hoiprodcl  46562  hoicvrrex  46571  ovnpnfelsup  46574  ovnlerp  46577  ovnf  46578  ovn0lem  46580  ovnsubaddlem1  46585  hoiprodcl3  46595  hoidmvcl  46597  sge0hsphoire  46604  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem4  46613  hoidmvlelem5  46614  ovnhoilem1  46616  volicorege0  46652  ovolval5lem1  46667  pimgtpnf2f  46720  pimiooltgt  46725  smfliminflem  46845  rrxsphere  48669  itscnhlinecirc02p  48706