Theorem pnfxr 11228

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 4142	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11227	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4726	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3943	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11212	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2827	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2109   ∪ cun 3912  {cpr 4591  ℝcr 11067  +∞cpnf 11205  -∞cmnf 11206  ℝ^*cxr 11207

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 5251  ax-pow 5320  ax-un 7711  ax-cnex 11124

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 3449  df-un 3919  df-ss 3931  df-pw 4565  df-sn 4590  df-pr 4592  df-uni 4872  df-pnf 11210  df-xr 11212

This theorem is referenced by:  pnfnemnf  11229  xnn0xr  12520  xrltnr  13079  ltpnf  13080  mnfltpnf  13086  pnfnlt  13088  pnfge  13090  nltpnft  13124  xgepnf  13125  xrre  13129  xrre2  13130  xnegcl  13173  xaddf  13184  xaddpnf1  13186  xaddpnf2  13187  pnfaddmnf  13190  mnfaddpnf  13191  xaddass2  13210  xlt2add  13220  xsubge0  13221  xmulneg1  13229  xmulf  13232  xmulpnf1  13234  xmulpnf2  13235  xmulmnf1  13236  xmulpnf1n  13238  xlemul1a  13248  xadddilem  13254  xadddi2  13257  xrsupsslem  13267  xrinfmsslem  13268  supxrpnf  13278  supxrunb1  13279  supxrunb2  13280  supxrbnd  13288  xrinf0  13299  dfrp2  13355  elicore  13359  elioc2  13370  elico2  13371  elicc2  13372  ioomax  13383  iccmax  13384  ioopos  13385  elioopnf  13404  elicopnf  13406  unirnioo  13410  xrge0neqmnf  13413  elxrge0  13418  difreicc  13445  xnn0xrge0  13467  ioopnfsup  13826  icopnfsup  13827  xrsup  13830  hashbnd  14301  hashnnn0genn0  14308  hashxrcl  14322  hashdomi  14345  sgnpnf  15059  rexico  15320  limsupgre  15447  rlim3  15464  fprodge0  15959  fprodge1  15961  pcxcl  16832  pc2dvds  16850  pcadd  16860  ramxrcl  16988  ramubcl  16989  xrsnsgrp  21319  xrsdsreclblem  21329  rge0srg  21355  leordtvallem1  23097  leordtval2  23099  lecldbas  23106  pnfnei  23107  mnfnei  23108  xblpnfps  24283  xblpnf  24284  xblss2ps  24289  blssec  24323  blpnfctr  24324  nmoix  24617  icopnfcld  24655  iocmnfcld  24656  xrtgioo  24695  reconnlem1  24715  xrge0tsms  24723  metdstri  24740  iccpnfcnv  24842  ovolf  25383  ovolicopnf  25425  ovolre  25426  volsup  25457  ioombl1lem4  25462  icombl1  25464  icombl  25465  ioombl  25466  uniioombllem1  25482  mbfdm  25527  ismbfd  25540  mbfmax  25550  ismbf3d  25555  itg2ge0  25636  lhop2  25920  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumrlim  25938  dvfsumrlim2  25939  taylfvallem1  26264  taylfval  26266  tayl0  26269  radcnvcl  26326  radcnvle  26329  psercnlem1  26335  logccv  26572  rlimcnp  26875  rlimcnp2  26876  xrlimcnp  26878  logfacbnd3  27134  chebbnd1  27383  chebbnd2  27388  dchrisumlem3  27402  log2sumbnd  27455  pntpbnd1  27497  pntibndlem2  27502  pntlemb  27508  pntleme  27519  pnt  27525  upgrfi  29018  topnfbey  30398  isblo3i  30730  xrge0infss  32683  xrdifh  32703  hashxpe  32732  elxrge02  32852  xdivpnfrp  32853  xrge0addass  32957  xrge0addgt0  32958  xrge0adddir  32959  xrge0npcan  32961  fsumrp0cl  32962  xrge0tsmsd  33002  pnfinf  33137  xrnarchi  33138  xrge0slmod  33319  unitssxrge0  33890  tpr2rico  33902  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  xrge0mulc1cn  33931  pnfneige0  33941  lmxrge0  33942  esumle  34048  esumlef  34052  esumcst  34053  esumpr2  34057  esumpinfval  34063  esumpinfsum  34067  esumpcvgval  34068  hashf2  34074  esumcvg  34076  esumcvgsum  34078  voliune  34219  volfiniune  34220  ddemeas  34226  sxbrsigalem0  34262  sxbrsigalem2  34277  oms0  34288  sibfinima  34330  sitmcl  34342  probmeasb  34421  orvcgteel  34459  dstfrvclim1  34469  signsply0  34542  chtvalz  34620  hgt750lemf  34644  iooelexlt  37350  mbfposadd  37661  itg2addnclem2  37666  ftc1anclem5  37691  asindmre  37697  dvasin  37698  dvacos  37699  aks4d1p1p6  42061  readvrec2  42349  readvrec  42350  dvconstbi  44323  rfcnpre3  45027  absfico  45212  xadd0ge  45317  xrgepnfd  45327  xrge0nemnfd  45328  supxrgere  45329  supxrgelem  45333  supxrge  45334  xralrple2  45350  infxr  45363  infleinflem2  45367  xrralrecnnge  45386  infxrpnf  45442  xrpnf  45481  iocopn  45518  pnfel0pnf  45526  ge0xrre  45529  ge0lere  45530  ressiooinf  45555  uzinico  45557  uzubioo  45563  fsumge0cl  45571  limcicciooub  45635  limsupre  45639  limcresiooub  45640  limcleqr  45642  limsupresre  45694  limsupresico  45698  limsuppnfdlem  45699  limsuppnflem  45708  limsupmnflem  45718  liminfresico  45769  limsup10exlem  45770  liminflelimsuplem  45773  liminflelimsupuz  45783  limsupub2  45810  liminflbuz2  45813  liminflimsupxrre  45815  xlimpnfvlem2  45835  xlimliminflimsup  45860  icccncfext  45885  iblsplit  45964  itgsubsticclem  45973  fourierdlem31  46136  fourierdlem33  46138  fourierdlem46  46150  fourierdlem47  46151  fourierdlem48  46152  fourierdlem49  46153  fourierdlem65  46169  fourierdlem73  46177  fourierdlem75  46179  fourierdlem85  46189  fourierdlem88  46192  fourierdlem95  46199  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  fourierdlem107  46211  fourierdlem109  46213  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  fouriersw  46229  ioorrnopnxrlem  46304  sge0val  46364  fge0iccico  46368  gsumge0cl  46369  sge0sn  46377  sge0tsms  46378  sge0cl  46379  sge0f1o  46380  sge0ge0  46382  sge0repnf  46384  sge0fsum  46385  sge0pr  46392  sge0prle  46399  sge0split  46407  sge0p1  46412  sge0iunmptlemre  46413  sge0rpcpnf  46419  sge0rernmpt  46420  sge0isum  46425  sge0ad2en  46429  sge0xaddlem1  46431  sge0xaddlem2  46432  sge0uzfsumgt  46442  sge0seq  46444  sge0reuz  46445  voliunsge0lem  46470  meage0  46473  meassre  46475  meaiuninclem  46478  omessre  46508  omeiunltfirp  46517  carageniuncllem2  46520  carageniuncl  46521  omege0  46531  hoiprodcl  46545  hoicvrrex  46554  ovnpnfelsup  46557  ovnlerp  46560  ovnf  46561  ovn0lem  46563  ovnsubaddlem1  46568  hoiprodcl3  46578  hoidmvcl  46580  sge0hsphoire  46587  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem4  46596  hoidmvlelem5  46597  ovnhoilem1  46599  volicorege0  46635  ovolval5lem1  46650  pimgtpnf2f  46703  pimiooltgt  46708  smfliminflem  46828  rehalfge1  47336  rrxsphere  48737  itscnhlinecirc02p  48774