Theorem pnfxr 11235

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 4145	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11234	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4729	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3946	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11219	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2828	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2109   ∪ cun 3915  {cpr 4594  ℝcr 11074  +∞cpnf 11212  -∞cmnf 11213  ℝ^*cxr 11214

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-pow 5323  ax-un 7714  ax-cnex 11131

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-pw 4568  df-sn 4593  df-pr 4595  df-uni 4875  df-pnf 11217  df-xr 11219

This theorem is referenced by:  pnfnemnf  11236  xnn0xr  12527  xrltnr  13086  ltpnf  13087  mnfltpnf  13093  pnfnlt  13095  pnfge  13097  nltpnft  13131  xgepnf  13132  xrre  13136  xrre2  13137  xnegcl  13180  xaddf  13191  xaddpnf1  13193  xaddpnf2  13194  pnfaddmnf  13197  mnfaddpnf  13198  xaddass2  13217  xlt2add  13227  xsubge0  13228  xmulneg1  13236  xmulf  13239  xmulpnf1  13241  xmulpnf2  13242  xmulmnf1  13243  xmulpnf1n  13245  xlemul1a  13255  xadddilem  13261  xadddi2  13264  xrsupsslem  13274  xrinfmsslem  13275  supxrpnf  13285  supxrunb1  13286  supxrunb2  13287  supxrbnd  13295  xrinf0  13306  dfrp2  13362  elicore  13366  elioc2  13377  elico2  13378  elicc2  13379  ioomax  13390  iccmax  13391  ioopos  13392  elioopnf  13411  elicopnf  13413  unirnioo  13417  xrge0neqmnf  13420  elxrge0  13425  difreicc  13452  xnn0xrge0  13474  ioopnfsup  13833  icopnfsup  13834  xrsup  13837  hashbnd  14308  hashnnn0genn0  14315  hashxrcl  14329  hashdomi  14352  sgnpnf  15066  rexico  15327  limsupgre  15454  rlim3  15471  fprodge0  15966  fprodge1  15968  pcxcl  16839  pc2dvds  16857  pcadd  16867  ramxrcl  16995  ramubcl  16996  xrsnsgrp  21326  xrsdsreclblem  21336  rge0srg  21362  leordtvallem1  23104  leordtval2  23106  lecldbas  23113  pnfnei  23114  mnfnei  23115  xblpnfps  24290  xblpnf  24291  xblss2ps  24296  blssec  24330  blpnfctr  24331  nmoix  24624  icopnfcld  24662  iocmnfcld  24663  xrtgioo  24702  reconnlem1  24722  xrge0tsms  24730  metdstri  24747  iccpnfcnv  24849  ovolf  25390  ovolicopnf  25432  ovolre  25433  volsup  25464  ioombl1lem4  25469  icombl1  25471  icombl  25472  ioombl  25473  uniioombllem1  25489  mbfdm  25534  ismbfd  25547  mbfmax  25557  ismbf3d  25562  itg2ge0  25643  lhop2  25927  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumrlim  25945  dvfsumrlim2  25946  taylfvallem1  26271  taylfval  26273  tayl0  26276  radcnvcl  26333  radcnvle  26336  psercnlem1  26342  logccv  26579  rlimcnp  26882  rlimcnp2  26883  xrlimcnp  26885  logfacbnd3  27141  chebbnd1  27390  chebbnd2  27395  dchrisumlem3  27409  log2sumbnd  27462  pntpbnd1  27504  pntibndlem2  27509  pntlemb  27515  pntleme  27526  pnt  27532  upgrfi  29025  topnfbey  30405  isblo3i  30737  xrge0infss  32690  xrdifh  32710  hashxpe  32739  elxrge02  32859  xdivpnfrp  32860  xrge0addass  32964  xrge0addgt0  32965  xrge0adddir  32966  xrge0npcan  32968  fsumrp0cl  32969  xrge0tsmsd  33009  pnfinf  33144  xrnarchi  33145  xrge0slmod  33326  unitssxrge0  33897  tpr2rico  33909  xrge0iifcnv  33930  xrge0iifiso  33932  xrge0iifhom  33934  xrge0mulc1cn  33938  pnfneige0  33948  lmxrge0  33949  esumle  34055  esumlef  34059  esumcst  34060  esumpr2  34064  esumpinfval  34070  esumpinfsum  34074  esumpcvgval  34075  hashf2  34081  esumcvg  34083  esumcvgsum  34085  voliune  34226  volfiniune  34227  ddemeas  34233  sxbrsigalem0  34269  sxbrsigalem2  34284  oms0  34295  sibfinima  34337  sitmcl  34349  probmeasb  34428  orvcgteel  34466  dstfrvclim1  34476  signsply0  34549  chtvalz  34627  hgt750lemf  34651  iooelexlt  37357  mbfposadd  37668  itg2addnclem2  37673  ftc1anclem5  37698  asindmre  37704  dvasin  37705  dvacos  37706  aks4d1p1p6  42068  readvrec2  42356  readvrec  42357  dvconstbi  44330  rfcnpre3  45034  absfico  45219  xadd0ge  45324  xrgepnfd  45334  xrge0nemnfd  45335  supxrgere  45336  supxrgelem  45340  supxrge  45341  xralrple2  45357  infxr  45370  infleinflem2  45374  xrralrecnnge  45393  infxrpnf  45449  xrpnf  45488  iocopn  45525  pnfel0pnf  45533  ge0xrre  45536  ge0lere  45537  ressiooinf  45562  uzinico  45564  uzubioo  45570  fsumge0cl  45578  limcicciooub  45642  limsupre  45646  limcresiooub  45647  limcleqr  45649  limsupresre  45701  limsupresico  45705  limsuppnfdlem  45706  limsuppnflem  45715  limsupmnflem  45725  liminfresico  45776  limsup10exlem  45777  liminflelimsuplem  45780  liminflelimsupuz  45790  limsupub2  45817  liminflbuz2  45820  liminflimsupxrre  45822  xlimpnfvlem2  45842  xlimliminflimsup  45867  icccncfext  45892  iblsplit  45971  itgsubsticclem  45980  fourierdlem31  46143  fourierdlem33  46145  fourierdlem46  46157  fourierdlem47  46158  fourierdlem48  46159  fourierdlem49  46160  fourierdlem65  46176  fourierdlem73  46184  fourierdlem75  46186  fourierdlem85  46196  fourierdlem88  46199  fourierdlem95  46206  fourierdlem97  46208  fourierdlem103  46214  fourierdlem104  46215  fourierdlem107  46218  fourierdlem109  46220  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  fouriersw  46236  ioorrnopnxrlem  46311  sge0val  46371  fge0iccico  46375  gsumge0cl  46376  sge0sn  46384  sge0tsms  46385  sge0cl  46386  sge0f1o  46387  sge0ge0  46389  sge0repnf  46391  sge0fsum  46392  sge0pr  46399  sge0prle  46406  sge0split  46414  sge0p1  46419  sge0iunmptlemre  46420  sge0rpcpnf  46426  sge0rernmpt  46427  sge0isum  46432  sge0ad2en  46436  sge0xaddlem1  46438  sge0xaddlem2  46439  sge0uzfsumgt  46449  sge0seq  46451  sge0reuz  46452  voliunsge0lem  46477  meage0  46480  meassre  46482  meaiuninclem  46485  omessre  46515  omeiunltfirp  46524  carageniuncllem2  46527  carageniuncl  46528  omege0  46538  hoiprodcl  46552  hoicvrrex  46561  ovnpnfelsup  46564  ovnlerp  46567  ovnf  46568  ovn0lem  46570  ovnsubaddlem1  46575  hoiprodcl3  46585  hoidmvcl  46587  sge0hsphoire  46594  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem4  46603  hoidmvlelem5  46604  ovnhoilem1  46606  volicorege0  46642  ovolval5lem1  46657  pimgtpnf2f  46710  pimiooltgt  46715  smfliminflem  46835  rehalfge1  47340  rrxsphere  48741  itscnhlinecirc02p  48778