Theorem pnfxr 11281

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 4135	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11280	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4733	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3937	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11265	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2865	1 ⊢ +∞ ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2146   ∪ cun 3906  {cpr 4596  ℝcr 11117  +∞cpnf 11258  -∞cmnf 11259  ℝ^*cxr 11260

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pow 5341  ax-un 7745  ax-cnex 11174

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-pw 4569  df-sn 4595  df-pr 4597  df-uni 4878  df-pnf 11263  df-xr 11265

This theorem is used by:  pnfnemnf  11282  xnn0xr  12600  xrltnr  13162  ltpnf  13163  mnfltpnf  13169  pnfnlt  13171  pnfge  13173  nltpnft  13208  xgepnf  13209  xrre  13213  xrre2  13214  xnegcl  13257  xaddf  13268  xaddpnf1  13270  xaddpnf2  13271  pnfaddmnf  13274  mnfaddpnf  13275  xaddass2  13294  xlt2add  13304  xsubge0  13305  xmulneg1  13313  xmulf  13316  xmulpnf1  13318  xmulpnf2  13319  xmulmnf1  13320  xmulpnf1n  13322  xlemul1a  13332  xadddilem  13338  xadddi2  13341  xrsupsslem  13351  xrinfmsslem  13352  supxrpnf  13362  supxrunb1  13363  supxrunb2  13364  supxrbnd  13372  xrinf0  13383  dfrp2  13439  elicore  13443  elioc2  13454  elico2  13455  elicc2  13456  ioomax  13467  iccmax  13468  ioopos  13469  elioopnf  13488  elicopnf  13490  unirnioo  13494  xrge0neqmnf  13497  elxrge0  13502  difreicc  13529  xnn0xrge0  13551  ioopnfsup  13917  icopnfsup  13918  xrsup  13921  hashbnd  14392  hashnnn0genn0  14399  hashxrcl  14413  hashdomi  14436  sgnpnf  15156  rexico  15431  limsupgre  15558  rlim3  15575  fprodge0  16073  fprodge1  16075  pcxcl  16946  pc2dvds  16964  pcadd  16974  ramxrcl  17102  ramubcl  17103  xrsnsgrp  21595  xrsdsreclblem  21600  rge0srg  21625  leordtvallem1  23404  leordtval2  23406  lecldbas  23413  pnfnei  23414  mnfnei  23415  xblpnfps  24589  xblpnf  24590  xblss2ps  24595  blssec  24629  blpnfctr  24630  nmoix  24923  icopnfcld  24961  iocmnfcld  24962  xrtgioo  25001  reconnlem1  25021  xrge0tsms  25029  metdstri  25046  iccpnfcnv  25140  ovolf  25678  ovolicopnf  25720  ovolre  25721  volsup  25752  ioombl1lem4  25757  icombl1  25759  icombl  25760  ioombl  25761  uniioombllem1  25777  mbfdm  25822  ismbfd  25835  mbfmax  25845  ismbf3d  25850  itg2ge0  25931  lhop2  26211  dvfsumlem2  26223  dvfsumrlim  26227  dvfsumrlim2  26228  taylfvallem1  26557  taylfval  26559  tayl0  26562  radcnvcl  26617  radcnvle  26620  psercnlem1  26625  logccv  26865  rlimcnp  27167  rlimcnp2  27168  xrlimcnp  27170  logfacbnd3  27424  chebbnd1  27673  chebbnd2  27678  dchrisumlem3  27692  log2sumbnd  27745  pntpbnd1  27787  pntibndlem2  27792  pntlemb  27798  pntleme  27809  pnt  27815  upgrfi  29478  topnfbey  30857  isblo3i  31190  xrge0infss  33142  xrdifh  33162  hashxpe  33189  elxrge02  33288  xdivpnfrp  33289  xrge0addass  33367  xrge0addgt0  33368  xrge0adddir  33369  xrge0npcan  33371  fsumrp0cl  33372  xrge0tsmsd  33424  pnfinf  33534  xrnarchi  33535  xrge0slmod  33699  unitssxrge0  34321  tpr2rico  34333  xrge0iifcnv  34354  xrge0iifiso  34356  xrge0iifhom  34358  xrge0mulc1cn  34362  pnfneige0  34372  lmxrge0  34373  esumle  34479  esumlef  34483  esumcst  34484  esumpr2  34488  esumpinfval  34494  esumpinfsum  34498  esumpcvgval  34499  hashf2  34505  esumcvg  34507  esumcvgsum  34509  voliune  34651  volfiniune  34652  ddemeas  34658  sxbrsigalem0  34693  sxbrsigalem2  34708  oms0  34719  sibfinima  34761  sitmcl  34773  probmeasb  34852  orvcgteel  34890  dstfrvclim1  34900  signsply0  34970  chtvalz  35048  hgt750lemf  35072  iooelexlt  38049  mbfposadd  38359  itg2addnclem2  38364  ftc1anclem5  38389  asindmre  38395  dvasin  38396  dvacos  38397  aks4d1p1p6  42881  readvrec2  43163  readvrec  43164  dvconstbi  45085  rfcnpre3  45794  absfico  45975  xadd0ge  46079  xrgepnfd  46088  xrge0nemnfd  46089  supxrgere  46090  supxrgelem  46094  supxrge  46095  xralrple2  46111  infxr  46123  infleinflem2  46127  xrralrecnnge  46146  infxrpnf  46201  xrpnf  46240  iocopn  46277  pnfel0pnf  46285  ge0xrre  46288  ge0lere  46289  ressiooinf  46314  uzinico  46316  uzubioo  46322  fsumge0cl  46330  limcicciooub  46392  limsupre  46396  limcresiooub  46397  limcleqr  46399  limsupresre  46451  limsupresico  46455  limsuppnfdlem  46456  limsuppnflem  46465  limsupmnflem  46475  liminfresico  46526  limsup10exlem  46527  liminflelimsuplem  46530  liminflelimsupuz  46540  limsupub2  46567  liminflbuz2  46570  liminflimsupxrre  46572  xlimpnfvlem2  46592  xlimliminflimsup  46617  icccncfext  46642  iblsplit  46721  itgsubsticclem  46730  fourierdlem31  46893  fourierdlem33  46895  fourierdlem46  46907  fourierdlem47  46908  fourierdlem48  46909  fourierdlem49  46910  fourierdlem65  46926  fourierdlem73  46934  fourierdlem75  46936  fourierdlem85  46946  fourierdlem88  46949  fourierdlem95  46956  fourierdlem97  46958  fourierdlem103  46964  fourierdlem104  46965  fourierdlem107  46968  fourierdlem109  46970  fourierdlem111  46972  fourierdlem112  46973  fourierdlem113  46974  fouriersw  46986  ioorrnopnxrlem  47061  sge0val  47121  fge0iccico  47125  gsumge0cl  47126  sge0sn  47134  sge0tsms  47135  sge0cl  47136  sge0f1o  47137  sge0ge0  47139  sge0repnf  47141  sge0fsum  47142  sge0pr  47149  sge0prle  47156  sge0split  47164  sge0p1  47169  sge0iunmptlemre  47170  sge0rpcpnf  47176  sge0rernmpt  47177  sge0isum  47182  sge0ad2en  47186  sge0xaddlem1  47188  sge0xaddlem2  47189  sge0uzfsumgt  47199  sge0seq  47201  sge0reuz  47202  voliunsge0lem  47227  meage0  47230  meassre  47232  meaiuninclem  47235  omessre  47265  omeiunltfirp  47274  carageniuncllem2  47277  carageniuncl  47278  omege0  47288  hoiprodcl  47302  hoicvrrex  47311  ovnpnfelsup  47314  ovnlerp  47317  ovnf  47318  ovn0lem  47320  ovnsubaddlem1  47325  hoiprodcl3  47335  hoidmvcl  47337  sge0hsphoire  47344  hoidmv1lelem1  47346  hoidmv1lelem2  47347  hoidmv1lelem3  47348  hoidmv1le  47349  hoidmvlelem1  47350  hoidmvlelem4  47353  hoidmvlelem5  47354  ovnhoilem1  47356  volicorege0  47392  ovolval5lem1  47407  pimgtpnf2f  47460  pimiooltgt  47465  smfliminflem  47585  rehalfge1  48117  rrxsphere  49569  itscnhlinecirc02p  49606