Theorem pnfxr 11188

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 4132	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11187	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4716	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3934	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11172	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2827	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2109   ∪ cun 3903  {cpr 4581  ℝcr 11027  +∞cpnf 11165  -∞cmnf 11166  ℝ^*cxr 11167

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 2701  ax-sep 5238  ax-pow 5307  ax-un 7675  ax-cnex 11084

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 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922  df-pw 4555  df-sn 4580  df-pr 4582  df-uni 4862  df-pnf 11170  df-xr 11172

This theorem is referenced by:  pnfnemnf  11189  xnn0xr  12480  xrltnr  13039  ltpnf  13040  mnfltpnf  13046  pnfnlt  13048  pnfge  13050  nltpnft  13084  xgepnf  13085  xrre  13089  xrre2  13090  xnegcl  13133  xaddf  13144  xaddpnf1  13146  xaddpnf2  13147  pnfaddmnf  13150  mnfaddpnf  13151  xaddass2  13170  xlt2add  13180  xsubge0  13181  xmulneg1  13189  xmulf  13192  xmulpnf1  13194  xmulpnf2  13195  xmulmnf1  13196  xmulpnf1n  13198  xlemul1a  13208  xadddilem  13214  xadddi2  13217  xrsupsslem  13227  xrinfmsslem  13228  supxrpnf  13238  supxrunb1  13239  supxrunb2  13240  supxrbnd  13248  xrinf0  13259  dfrp2  13315  elicore  13319  elioc2  13330  elico2  13331  elicc2  13332  ioomax  13343  iccmax  13344  ioopos  13345  elioopnf  13364  elicopnf  13366  unirnioo  13370  xrge0neqmnf  13373  elxrge0  13378  difreicc  13405  xnn0xrge0  13427  ioopnfsup  13786  icopnfsup  13787  xrsup  13790  hashbnd  14261  hashnnn0genn0  14268  hashxrcl  14282  hashdomi  14305  sgnpnf  15018  rexico  15279  limsupgre  15406  rlim3  15423  fprodge0  15918  fprodge1  15920  pcxcl  16791  pc2dvds  16809  pcadd  16819  ramxrcl  16947  ramubcl  16948  xrsnsgrp  21332  xrsdsreclblem  21337  rge0srg  21363  leordtvallem1  23113  leordtval2  23115  lecldbas  23122  pnfnei  23123  mnfnei  23124  xblpnfps  24299  xblpnf  24300  xblss2ps  24305  blssec  24339  blpnfctr  24340  nmoix  24633  icopnfcld  24671  iocmnfcld  24672  xrtgioo  24711  reconnlem1  24731  xrge0tsms  24739  metdstri  24756  iccpnfcnv  24858  ovolf  25399  ovolicopnf  25441  ovolre  25442  volsup  25473  ioombl1lem4  25478  icombl1  25480  icombl  25481  ioombl  25482  uniioombllem1  25498  mbfdm  25543  ismbfd  25556  mbfmax  25566  ismbf3d  25571  itg2ge0  25652  lhop2  25936  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsumrlim  25954  dvfsumrlim2  25955  taylfvallem1  26280  taylfval  26282  tayl0  26285  radcnvcl  26342  radcnvle  26345  psercnlem1  26351  logccv  26588  rlimcnp  26891  rlimcnp2  26892  xrlimcnp  26894  logfacbnd3  27150  chebbnd1  27399  chebbnd2  27404  dchrisumlem3  27418  log2sumbnd  27471  pntpbnd1  27513  pntibndlem2  27518  pntlemb  27524  pntleme  27535  pnt  27541  upgrfi  29054  topnfbey  30431  isblo3i  30763  xrge0infss  32716  xrdifh  32736  hashxpe  32765  elxrge02  32885  xdivpnfrp  32886  xrge0addass  32983  xrge0addgt0  32984  xrge0adddir  32985  xrge0npcan  32987  fsumrp0cl  32988  xrge0tsmsd  33028  pnfinf  33135  xrnarchi  33136  xrge0slmod  33295  unitssxrge0  33866  tpr2rico  33878  xrge0iifcnv  33899  xrge0iifiso  33901  xrge0iifhom  33903  xrge0mulc1cn  33907  pnfneige0  33917  lmxrge0  33918  esumle  34024  esumlef  34028  esumcst  34029  esumpr2  34033  esumpinfval  34039  esumpinfsum  34043  esumpcvgval  34044  hashf2  34050  esumcvg  34052  esumcvgsum  34054  voliune  34195  volfiniune  34196  ddemeas  34202  sxbrsigalem0  34238  sxbrsigalem2  34253  oms0  34264  sibfinima  34306  sitmcl  34318  probmeasb  34397  orvcgteel  34435  dstfrvclim1  34445  signsply0  34518  chtvalz  34596  hgt750lemf  34620  iooelexlt  37335  mbfposadd  37646  itg2addnclem2  37651  ftc1anclem5  37676  asindmre  37682  dvasin  37683  dvacos  37684  aks4d1p1p6  42046  readvrec2  42334  readvrec  42335  dvconstbi  44307  rfcnpre3  45011  absfico  45196  xadd0ge  45301  xrgepnfd  45311  xrge0nemnfd  45312  supxrgere  45313  supxrgelem  45317  supxrge  45318  xralrple2  45334  infxr  45347  infleinflem2  45351  xrralrecnnge  45370  infxrpnf  45426  xrpnf  45465  iocopn  45502  pnfel0pnf  45510  ge0xrre  45513  ge0lere  45514  ressiooinf  45539  uzinico  45541  uzubioo  45547  fsumge0cl  45555  limcicciooub  45619  limsupre  45623  limcresiooub  45624  limcleqr  45626  limsupresre  45678  limsupresico  45682  limsuppnfdlem  45683  limsuppnflem  45692  limsupmnflem  45702  liminfresico  45753  limsup10exlem  45754  liminflelimsuplem  45757  liminflelimsupuz  45767  limsupub2  45794  liminflbuz2  45797  liminflimsupxrre  45799  xlimpnfvlem2  45819  xlimliminflimsup  45844  icccncfext  45869  iblsplit  45948  itgsubsticclem  45957  fourierdlem31  46120  fourierdlem33  46122  fourierdlem46  46134  fourierdlem47  46135  fourierdlem48  46136  fourierdlem49  46137  fourierdlem65  46153  fourierdlem73  46161  fourierdlem75  46163  fourierdlem85  46173  fourierdlem88  46176  fourierdlem95  46183  fourierdlem97  46185  fourierdlem103  46191  fourierdlem104  46192  fourierdlem107  46195  fourierdlem109  46197  fourierdlem111  46199  fourierdlem112  46200  fourierdlem113  46201  fouriersw  46213  ioorrnopnxrlem  46288  sge0val  46348  fge0iccico  46352  gsumge0cl  46353  sge0sn  46361  sge0tsms  46362  sge0cl  46363  sge0f1o  46364  sge0ge0  46366  sge0repnf  46368  sge0fsum  46369  sge0pr  46376  sge0prle  46383  sge0split  46391  sge0p1  46396  sge0iunmptlemre  46397  sge0rpcpnf  46403  sge0rernmpt  46404  sge0isum  46409  sge0ad2en  46413  sge0xaddlem1  46415  sge0xaddlem2  46416  sge0uzfsumgt  46426  sge0seq  46428  sge0reuz  46429  voliunsge0lem  46454  meage0  46457  meassre  46459  meaiuninclem  46462  omessre  46492  omeiunltfirp  46501  carageniuncllem2  46504  carageniuncl  46505  omege0  46515  hoiprodcl  46529  hoicvrrex  46538  ovnpnfelsup  46541  ovnlerp  46544  ovnf  46545  ovn0lem  46547  ovnsubaddlem1  46552  hoiprodcl3  46562  hoidmvcl  46564  sge0hsphoire  46571  hoidmv1lelem1  46573  hoidmv1lelem2  46574  hoidmv1lelem3  46575  hoidmv1le  46576  hoidmvlelem1  46577  hoidmvlelem4  46580  hoidmvlelem5  46581  ovnhoilem1  46583  volicorege0  46619  ovolval5lem1  46634  pimgtpnf2f  46687  pimiooltgt  46692  smfliminflem  46812  rehalfge1  47320  rrxsphere  48734  itscnhlinecirc02p  48771