Theorem pnfxr 10410

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 4004	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 10409	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4515	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3824	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 10395	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2905	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2166   ∪ cun 3796  {cpr 4399  ℝcr 10251  +∞cpnf 10388  -∞cmnf 10389  ℝ^*cxr 10390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803  ax-sep 5005  ax-pow 5065  ax-un 7209  ax-cnex 10308

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-v 3416  df-un 3803  df-in 3805  df-ss 3812  df-pw 4380  df-sn 4398  df-pr 4400  df-uni 4659  df-pnf 10393  df-xr 10395

This theorem is referenced by:  pnfexOLD  10411  pnfnemnf  10412  xnn0xr  11695  xrltnr  12239  ltpnf  12240  mnfltpnf  12246  pnfnlt  12248  pnfge  12250  nltpnft  12283  xgepnf  12284  xrre  12288  xrre2  12289  xnegcl  12332  xaddf  12343  xaddpnf1  12345  xaddpnf2  12346  pnfaddmnf  12349  mnfaddpnf  12350  xaddass2  12368  xlt2add  12378  xsubge0  12379  xmulneg1  12387  xmulf  12390  xmulpnf1  12392  xmulpnf2  12393  xmulmnf1  12394  xmulpnf1n  12396  xlemul1a  12406  xadddilem  12412  xadddi2  12415  xrsupsslem  12425  xrinfmsslem  12426  supxrpnf  12436  supxrunb1  12437  supxrunb2  12438  supxrbnd  12446  xrinf0  12456  elicore  12514  elioc2  12524  elico2  12525  elicc2  12526  ioomax  12536  iccmax  12537  ioopos  12538  elioopnf  12556  elicopnf  12558  unirnioo  12562  xrge0neqmnf  12565  xrge0neqmnfOLD  12566  elxrge0  12571  difreicc  12597  xnn0xrge0  12618  ioopnfsup  12958  icopnfsup  12959  xrsup  12962  hashbnd  13416  hashnnn0genn0  13423  hashxrcl  13438  hashdomi  13459  sgnpnf  14210  rexico  14470  limsupgre  14589  rlim3  14606  fprodge0  15096  fprodge1  15098  pcxcl  15936  pc2dvds  15954  pcadd  15964  ramxrcl  16092  ramubcl  16093  xrsnsgrp  20142  xrsdsreclblem  20152  rge0srg  20177  leordtvallem1  21385  leordtval2  21387  lecldbas  21394  pnfnei  21395  mnfnei  21396  xblpnfps  22570  xblpnf  22571  xblss2ps  22576  blssec  22610  blpnfctr  22611  nmoix  22903  icopnfcld  22941  iocmnfcld  22942  xrtgioo  22979  reconnlem1  22999  xrge0tsms  23007  metdstri  23024  iccpnfcnv  23113  ovolf  23648  ovolicopnf  23690  ovolre  23691  volsup  23722  ioombl1lem4  23727  icombl1  23729  icombl  23730  ioombl  23731  uniioombllem1  23747  mbfdm  23792  ismbfd  23805  mbfmax  23815  ismbf3d  23820  itg2ge0  23901  lhop2  24177  dvfsumlem2  24189  dvfsumrlim  24193  dvfsumrlim2  24194  taylfvallem1  24510  taylfval  24512  tayl0  24515  radcnvcl  24570  radcnvle  24573  psercnlem1  24578  logccv  24808  rlimcnp  25105  rlimcnp2  25106  xrlimcnp  25108  logfacbnd3  25361  chebbnd1  25574  chebbnd2  25579  dchrisumlem3  25593  log2sumbnd  25646  pntpbnd1  25688  pntibndlem2  25693  pntlemb  25699  pntleme  25710  pnt  25716  upgrfi  26389  topnfbey  27883  isblo3i  28211  xrge0infss  30072  dfrp2  30079  xrdifh  30089  elxrge02  30185  xdivpnfrp  30186  xrge0addass  30235  xrge0addgt0  30236  xrge0adddir  30237  xrge0npcan  30239  fsumrp0cl  30240  pnfinf  30282  xrnarchi  30283  xrge0tsmsd  30330  xrge0slmod  30389  unitssxrge0  30491  tpr2rico  30503  xrge0iifcnv  30524  xrge0iifiso  30526  xrge0iifhom  30528  xrge0mulc1cn  30532  pnfneige0  30542  lmxrge0  30543  esumle  30665  esumlef  30669  esumcst  30670  esumpr2  30674  esumpinfval  30680  esumpinfsum  30684  esumpcvgval  30685  hashf2  30691  esumcvg  30693  esumcvgsum  30695  voliune  30837  volfiniune  30838  ddemeas  30844  sxbrsigalem0  30878  sxbrsigalem2  30893  oms0  30904  sibfinima  30946  sitmcl  30958  probmeasb  31038  orvcgteel  31075  dstfrvclim1  31085  signsply0  31175  chtvalz  31256  hgt750lemf  31280  iooelexlt  33755  mbfposadd  34000  itg2addnclem2  34005  ftc1anclem5  34032  asindmre  34038  dvasin  34039  dvacos  34040  dvconstbi  39373  rfcnpre3  40010  absfico  40216  xadd0ge  40333  xrgepnfd  40344  xrge0nemnfd  40345  supxrgere  40346  supxrgelem  40350  supxrge  40351  xralrple2  40367  infxr  40380  infleinflem2  40384  xrralrecnnge  40408  infxrpnf  40469  xrpnf  40510  iocopn  40542  pnfel0pnf  40550  ge0xrre  40553  ge0lere  40554  ressiooinf  40579  uzinico  40582  uzubioo  40589  fsumge0cl  40600  limcicciooub  40664  limsupre  40668  limcresiooub  40669  limcleqr  40671  limsupresre  40723  limsupresico  40727  limsuppnfdlem  40728  limsuppnflem  40737  limsupmnflem  40747  liminfresico  40798  limsup10exlem  40799  liminflelimsuplem  40802  liminflelimsupuz  40812  xlimpnfvlem2  40858  icccncfext  40895  iblsplit  40976  itgsubsticclem  40985  fourierdlem31  41149  fourierdlem33  41151  fourierdlem46  41163  fourierdlem47  41164  fourierdlem48  41165  fourierdlem49  41166  fourierdlem65  41182  fourierdlem73  41190  fourierdlem75  41192  fourierdlem85  41202  fourierdlem88  41205  fourierdlem95  41212  fourierdlem97  41214  fourierdlem103  41220  fourierdlem104  41221  fourierdlem107  41224  fourierdlem109  41226  fourierdlem111  41228  fourierdlem112  41229  fourierdlem113  41230  fouriersw  41242  ioorrnopnxrlem  41317  sge0val  41374  fge0iccico  41378  gsumge0cl  41379  sge0sn  41387  sge0tsms  41388  sge0cl  41389  sge0f1o  41390  sge0ge0  41392  sge0repnf  41394  sge0fsum  41395  sge0pr  41402  sge0prle  41409  sge0split  41417  sge0p1  41422  sge0iunmptlemre  41423  sge0rpcpnf  41429  sge0rernmpt  41430  sge0isum  41435  sge0ad2en  41439  sge0xaddlem1  41441  sge0xaddlem2  41442  sge0uzfsumgt  41452  sge0seq  41454  sge0reuz  41455  voliunsge0lem  41480  meage0  41483  meassre  41485  meaiuninclem  41488  omessre  41518  omeiunltfirp  41527  carageniuncllem2  41530  carageniuncl  41531  omege0  41541  hoiprodcl  41555  hoicvrrex  41564  ovnpnfelsup  41567  ovnlerp  41570  ovnf  41571  ovn0lem  41573  ovnsubaddlem1  41578  hoiprodcl3  41588  hoidmvcl  41590  sge0hsphoire  41597  hoidmv1lelem1  41599  hoidmv1lelem2  41600  hoidmv1lelem3  41601  hoidmv1le  41602  hoidmvlelem1  41603  hoidmvlelem4  41606  hoidmvlelem5  41607  ovnhoilem1  41609  volicorege0  41645  ovolval5lem1  41660  pimgtpnf2  41711  pimiooltgt  41715  smfliminflem  41830  rrxsphere  43300