Theorem pnfxr 11344

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 4125	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11343	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4723	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3928	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11328	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2860	1 ⊢ +∞ ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2145   ∪ cun 3897  {cpr 4586  ℝcr 11180  +∞cpnf 11321  -∞cmnf 11322  ℝ^*cxr 11323

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-un 7740  ax-cnex 11237

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-pw 4559  df-sn 4585  df-pr 4587  df-uni 4868  df-pnf 11326  df-xr 11328

This theorem is used by:  pnfnemnf  11345  xnn0xr  12665  xrltnr  13229  ltpnf  13230  mnfltpnf  13236  pnfnlt  13238  pnfge  13240  nltpnft  13275  xgepnf  13276  xrre  13280  xrre2  13281  xnegcl  13324  xaddf  13335  xaddpnf1  13337  xaddpnf2  13338  pnfaddmnf  13341  mnfaddpnf  13342  xaddass2  13361  xlt2add  13371  xsubge0  13372  xmulneg1  13380  xmulf  13383  xmulpnf1  13385  xmulpnf2  13386  xmulmnf1  13387  xmulpnf1n  13389  xlemul1a  13399  xadddilem  13405  xadddi2  13408  xrsupsslem  13418  xrinfmsslem  13419  supxrpnf  13429  supxrunb1  13430  supxrunb2  13431  supxrbnd  13439  xrinf0  13450  dfrp2  13506  elicore  13510  elioc2  13521  elico2  13522  elicc2  13523  ioomax  13534  iccmax  13535  ioopos  13536  elioopnf  13555  elicopnf  13557  unirnioo  13561  xrge0neqmnf  13564  elxrge0  13569  difreicc  13596  xnn0xrge0  13618  ioopnfsup  13984  icopnfsup  13985  xrsup  13988  hashbnd  14460  hashnnn0genn0  14467  hashxrcl  14481  hashdomi  14504  sgnpnf  15226  rexico  15501  limsupgre  15628  rlim3  15645  fprodge0  16140  fprodge1  16142  pcxcl  17019  pc2dvds  17037  pcadd  17047  ramxrcl  17175  ramubcl  17176  xrsnsgrp  21694  xrsdsreclblem  21699  rge0srg  21724  leordtvallem1  23508  leordtval2  23510  lecldbas  23517  pnfnei  23518  mnfnei  23519  xblpnfps  24694  xblpnf  24695  xblss2ps  24700  blssec  24734  blpnfctr  24735  nmoix  25028  icopnfcld  25066  iocmnfcld  25067  xrtgioo  25106  reconnlem1  25126  xrge0tsms  25134  metdstri  25151  iccpnfcnv  25245  ovolf  25783  ovolicopnf  25825  ovolre  25826  volsup  25857  ioombl1lem4  25862  icombl1  25864  icombl  25865  ioombl  25866  uniioombllem1  25882  mbfdm  25927  ismbfd  25940  mbfmax  25950  ismbf3d  25955  itg2ge0  26036  lhop2  26315  dvfsumlem2  26327  dvfsumrlim  26331  dvfsumrlim2  26332  taylfvallem1  26666  taylfval  26668  tayl0  26671  radcnvcl  26726  radcnvle  26729  psercnlem1  26734  logccv  26973  rlimcnp  27275  rlimcnp2  27276  xrlimcnp  27278  logfacbnd3  27532  chebbnd1  27781  chebbnd2  27786  dchrisumlem3  27800  log2sumbnd  27853  pntpbnd1  27895  pntibndlem2  27900  pntlemb  27906  pntleme  27917  pnt  27923  upgrfi  29651  topnfbey  31052  isblo3i  31385  xrge0infss  33334  xrdifh  33354  hashxpe  33381  elxrge02  33480  xdivpnfrp  33481  xrge0addass  33559  xrge0addgt0  33560  xrge0adddir  33561  xrge0npcan  33563  fsumrp0cl  33564  xrge0tsmsd  33616  pnfinf  33726  xrnarchi  33727  xrge0slmod  33891  unitssxrge0  34514  tpr2rico  34526  xrge0iifcnv  34547  xrge0iifiso  34549  xrge0iifhom  34551  xrge0mulc1cn  34555  pnfneige0  34565  lmxrge0  34566  esumle  34672  esumlef  34676  esumcst  34677  esumpr2  34681  esumpinfval  34687  esumpinfsum  34691  esumpcvgval  34692  hashf2  34698  esumcvg  34700  esumcvgsum  34702  voliune  34844  volfiniune  34845  ddemeas  34851  sxbrsigalem0  34886  sxbrsigalem2  34901  oms0  34912  sibfinima  34954  sitmcl  34966  probmeasb  35045  orvcgteel  35083  dstfrvclim1  35093  signsply0  35163  chtvalz  35241  hgt750lemf  35265  iooelexlt  38253  mbfposadd  38553  itg2addnclem2  38558  ftc1anclem5  38583  asindmre  38589  dvasin  38590  dvacos  38591  aks4d1p1p6  43091  readvrec2  43380  readvrec  43381  dvconstbi  45277  rfcnpre3  45993  absfico  46174  xadd0ge  46278  xrgepnfd  46287  xrge0nemnfd  46288  supxrgere  46289  supxrgelem  46293  supxrge  46294  xralrple2  46310  infxr  46322  infleinflem2  46326  xrralrecnnge  46345  infxrpnf  46400  xrpnf  46439  iocopn  46476  pnfel0pnf  46484  ge0xrre  46487  ge0lere  46488  ressiooinf  46513  uzinico  46515  uzubioo  46521  fsumge0cl  46529  limcicciooub  46591  limsupre  46595  limcresiooub  46596  limcleqr  46598  limsupresre  46650  limsupresico  46654  limsuppnfdlem  46655  limsuppnflem  46664  limsupmnflem  46674  liminfresico  46725  limsup10exlem  46726  liminflelimsuplem  46729  liminflelimsupuz  46739  limsupub2  46766  liminflbuz2  46769  liminflimsupxrre  46771  xlimpnfvlem2  46791  xlimliminflimsup  46816  icccncfext  46841  iblsplit  46920  itgsubsticclem  46929  fourierdlem31  47092  fourierdlem33  47094  fourierdlem46  47106  fourierdlem47  47107  fourierdlem48  47108  fourierdlem49  47109  fourierdlem65  47125  fourierdlem73  47133  fourierdlem75  47135  fourierdlem85  47145  fourierdlem88  47148  fourierdlem95  47155  fourierdlem97  47157  fourierdlem103  47163  fourierdlem104  47164  fourierdlem107  47167  fourierdlem109  47169  fourierdlem111  47171  fourierdlem112  47172  fourierdlem113  47173  fouriersw  47185  ioorrnopnxrlem  47260  sge0val  47320  fge0iccico  47324  gsumge0cl  47325  sge0sn  47333  sge0tsms  47334  sge0cl  47335  sge0f1o  47336  sge0ge0  47338  sge0repnf  47340  sge0fsum  47341  sge0pr  47348  sge0prle  47355  sge0split  47363  sge0p1  47368  sge0iunmptlemre  47369  sge0rpcpnf  47375  sge0rernmpt  47376  sge0isum  47381  sge0ad2en  47385  sge0xaddlem1  47387  sge0xaddlem2  47388  sge0uzfsumgt  47398  sge0seq  47400  sge0reuz  47401  voliunsge0lem  47426  meage0  47429  meassre  47431  meaiuninclem  47434  omessre  47464  omeiunltfirp  47473  carageniuncllem2  47476  carageniuncl  47477  omege0  47487  hoiprodcl  47501  hoicvrrex  47510  ovnpnfelsup  47513  ovnlerp  47516  ovnf  47517  ovn0lem  47519  ovnsubaddlem1  47524  hoiprodcl3  47534  hoidmvcl  47536  sge0hsphoire  47543  hoidmv1lelem1  47545  hoidmv1lelem2  47546  hoidmv1lelem3  47547  hoidmv1le  47548  hoidmvlelem1  47549  hoidmvlelem4  47552  hoidmvlelem5  47553  ovnhoilem1  47555  volicorege0  47591  ovolval5lem1  47606  pimgtpnf2f  47659  pimiooltgt  47664  smfliminflem  47784  rehalfge1  48353  rrxsphere  49804  itscnhlinecirc02p  49841