Theorem pnfxr 11038

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 4108	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11037	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4699	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3919	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11022	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2839	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2107   ∪ cun 3886  {cpr 4564  ℝcr 10879  +∞cpnf 11015  -∞cmnf 11016  ℝ^*cxr 11017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-pow 5289  ax-un 7597  ax-cnex 10936

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-in 3895  df-ss 3905  df-pw 4536  df-sn 4563  df-pr 4565  df-uni 4841  df-pnf 11020  df-xr 11022

This theorem is referenced by:  pnfnemnf  11039  xnn0xr  12319  xrltnr  12864  ltpnf  12865  mnfltpnf  12871  pnfnlt  12873  pnfge  12875  nltpnft  12907  xgepnf  12908  xrre  12912  xrre2  12913  xnegcl  12956  xaddf  12967  xaddpnf1  12969  xaddpnf2  12970  pnfaddmnf  12973  mnfaddpnf  12974  xaddass2  12993  xlt2add  13003  xsubge0  13004  xmulneg1  13012  xmulf  13015  xmulpnf1  13017  xmulpnf2  13018  xmulmnf1  13019  xmulpnf1n  13021  xlemul1a  13031  xadddilem  13037  xadddi2  13040  xrsupsslem  13050  xrinfmsslem  13051  supxrpnf  13061  supxrunb1  13062  supxrunb2  13063  supxrbnd  13071  xrinf0  13081  dfrp2  13137  elicore  13140  elioc2  13151  elico2  13152  elicc2  13153  ioomax  13163  iccmax  13164  ioopos  13165  elioopnf  13184  elicopnf  13186  unirnioo  13190  xrge0neqmnf  13193  elxrge0  13198  difreicc  13225  xnn0xrge0  13247  ioopnfsup  13593  icopnfsup  13594  xrsup  13597  hashbnd  14059  hashnnn0genn0  14066  hashxrcl  14081  hashdomi  14104  sgnpnf  14813  rexico  15074  limsupgre  15199  rlim3  15216  fprodge0  15712  fprodge1  15714  pcxcl  16571  pc2dvds  16589  pcadd  16599  ramxrcl  16727  ramubcl  16728  xrsnsgrp  20643  xrsdsreclblem  20653  rge0srg  20678  leordtvallem1  22370  leordtval2  22372  lecldbas  22379  pnfnei  22380  mnfnei  22381  xblpnfps  23557  xblpnf  23558  xblss2ps  23563  blssec  23597  blpnfctr  23598  nmoix  23902  icopnfcld  23940  iocmnfcld  23941  xrtgioo  23978  reconnlem1  23998  xrge0tsms  24006  metdstri  24023  iccpnfcnv  24116  ovolf  24655  ovolicopnf  24697  ovolre  24698  volsup  24729  ioombl1lem4  24734  icombl1  24736  icombl  24737  ioombl  24738  uniioombllem1  24754  mbfdm  24799  ismbfd  24812  mbfmax  24822  ismbf3d  24827  itg2ge0  24909  lhop2  25188  dvfsumlem2  25200  dvfsumrlim  25204  dvfsumrlim2  25205  taylfvallem1  25525  taylfval  25527  tayl0  25530  radcnvcl  25585  radcnvle  25588  psercnlem1  25593  logccv  25827  rlimcnp  26124  rlimcnp2  26125  xrlimcnp  26127  logfacbnd3  26380  chebbnd1  26629  chebbnd2  26634  dchrisumlem3  26648  log2sumbnd  26701  pntpbnd1  26743  pntibndlem2  26748  pntlemb  26754  pntleme  26765  pnt  26771  upgrfi  27470  topnfbey  28842  isblo3i  29172  xrge0infss  31092  xrdifh  31110  hashxpe  31136  elxrge02  31215  xdivpnfrp  31216  xrge0addass  31308  xrge0addgt0  31309  xrge0adddir  31310  xrge0npcan  31312  fsumrp0cl  31313  xrge0tsmsd  31326  pnfinf  31446  xrnarchi  31447  xrge0slmod  31557  unitssxrge0  31859  tpr2rico  31871  xrge0iifcnv  31892  xrge0iifiso  31894  xrge0iifhom  31896  xrge0mulc1cn  31900  pnfneige0  31910  lmxrge0  31911  esumle  32035  esumlef  32039  esumcst  32040  esumpr2  32044  esumpinfval  32050  esumpinfsum  32054  esumpcvgval  32055  hashf2  32061  esumcvg  32063  esumcvgsum  32065  voliune  32206  volfiniune  32207  ddemeas  32213  sxbrsigalem0  32247  sxbrsigalem2  32262  oms0  32273  sibfinima  32315  sitmcl  32327  probmeasb  32406  orvcgteel  32443  dstfrvclim1  32453  signsply0  32539  chtvalz  32618  hgt750lemf  32642  iooelexlt  35542  mbfposadd  35833  itg2addnclem2  35838  ftc1anclem5  35863  asindmre  35869  dvasin  35870  dvacos  35871  aks4d1p1p6  40088  dvconstbi  41959  rfcnpre3  42583  absfico  42765  xadd0ge  42866  xrgepnfd  42877  xrge0nemnfd  42878  supxrgere  42879  supxrgelem  42883  supxrge  42884  xralrple2  42900  infxr  42913  infleinflem2  42917  xrralrecnnge  42937  infxrpnf  42993  xrpnf  43033  iocopn  43065  pnfel0pnf  43073  ge0xrre  43076  ge0lere  43077  ressiooinf  43102  uzinico  43105  uzubioo  43112  fsumge0cl  43121  limcicciooub  43185  limsupre  43189  limcresiooub  43190  limcleqr  43192  limsupresre  43244  limsupresico  43248  limsuppnfdlem  43249  limsuppnflem  43258  limsupmnflem  43268  liminfresico  43319  limsup10exlem  43320  liminflelimsuplem  43323  liminflelimsupuz  43333  limsupub2  43360  liminflbuz2  43363  liminflimsupxrre  43365  xlimpnfvlem2  43385  xlimliminflimsup  43410  icccncfext  43435  iblsplit  43514  itgsubsticclem  43523  fourierdlem31  43686  fourierdlem33  43688  fourierdlem46  43700  fourierdlem47  43701  fourierdlem48  43702  fourierdlem49  43703  fourierdlem65  43719  fourierdlem73  43727  fourierdlem75  43729  fourierdlem85  43739  fourierdlem88  43742  fourierdlem95  43749  fourierdlem97  43751  fourierdlem103  43757  fourierdlem104  43758  fourierdlem107  43761  fourierdlem109  43763  fourierdlem111  43765  fourierdlem112  43766  fourierdlem113  43767  fouriersw  43779  ioorrnopnxrlem  43854  sge0val  43911  fge0iccico  43915  gsumge0cl  43916  sge0sn  43924  sge0tsms  43925  sge0cl  43926  sge0f1o  43927  sge0ge0  43929  sge0repnf  43931  sge0fsum  43932  sge0pr  43939  sge0prle  43946  sge0split  43954  sge0p1  43959  sge0iunmptlemre  43960  sge0rpcpnf  43966  sge0rernmpt  43967  sge0isum  43972  sge0ad2en  43976  sge0xaddlem1  43978  sge0xaddlem2  43979  sge0uzfsumgt  43989  sge0seq  43991  sge0reuz  43992  voliunsge0lem  44017  meage0  44020  meassre  44022  meaiuninclem  44025  omessre  44055  omeiunltfirp  44064  carageniuncllem2  44067  carageniuncl  44068  omege0  44078  hoiprodcl  44092  hoicvrrex  44101  ovnpnfelsup  44104  ovnlerp  44107  ovnf  44108  ovn0lem  44110  ovnsubaddlem1  44115  hoiprodcl3  44125  hoidmvcl  44127  sge0hsphoire  44134  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmv1le  44139  hoidmvlelem1  44140  hoidmvlelem4  44143  hoidmvlelem5  44144  ovnhoilem1  44146  volicorege0  44182  ovolval5lem1  44197  pimgtpnf2f  44250  pimiooltgt  44255  smfliminflem  44374  rrxsphere  46105  itscnhlinecirc02p  46142