Theorem pnfxr 11173

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 4128	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11172	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4714	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3927	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11157	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2832	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2113   ∪ cun 3896  {cpr 4577  ℝcr 11012  +∞cpnf 11150  -∞cmnf 11151  ℝ^*cxr 11152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-pow 5305  ax-un 7674  ax-cnex 11069

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-pw 4551  df-sn 4576  df-pr 4578  df-uni 4859  df-pnf 11155  df-xr 11157

This theorem is referenced by:  pnfnemnf  11174  xnn0xr  12466  xrltnr  13020  ltpnf  13021  mnfltpnf  13027  pnfnlt  13029  pnfge  13031  nltpnft  13065  xgepnf  13066  xrre  13070  xrre2  13071  xnegcl  13114  xaddf  13125  xaddpnf1  13127  xaddpnf2  13128  pnfaddmnf  13131  mnfaddpnf  13132  xaddass2  13151  xlt2add  13161  xsubge0  13162  xmulneg1  13170  xmulf  13173  xmulpnf1  13175  xmulpnf2  13176  xmulmnf1  13177  xmulpnf1n  13179  xlemul1a  13189  xadddilem  13195  xadddi2  13198  xrsupsslem  13208  xrinfmsslem  13209  supxrpnf  13219  supxrunb1  13220  supxrunb2  13221  supxrbnd  13229  xrinf0  13240  dfrp2  13296  elicore  13300  elioc2  13311  elico2  13312  elicc2  13313  ioomax  13324  iccmax  13325  ioopos  13326  elioopnf  13345  elicopnf  13347  unirnioo  13351  xrge0neqmnf  13354  elxrge0  13359  difreicc  13386  xnn0xrge0  13408  ioopnfsup  13770  icopnfsup  13771  xrsup  13774  hashbnd  14245  hashnnn0genn0  14252  hashxrcl  14266  hashdomi  14289  sgnpnf  15002  rexico  15263  limsupgre  15390  rlim3  15407  fprodge0  15902  fprodge1  15904  pcxcl  16775  pc2dvds  16793  pcadd  16803  ramxrcl  16931  ramubcl  16932  xrsnsgrp  21346  xrsdsreclblem  21351  rge0srg  21377  leordtvallem1  23126  leordtval2  23128  lecldbas  23135  pnfnei  23136  mnfnei  23137  xblpnfps  24311  xblpnf  24312  xblss2ps  24317  blssec  24351  blpnfctr  24352  nmoix  24645  icopnfcld  24683  iocmnfcld  24684  xrtgioo  24723  reconnlem1  24743  xrge0tsms  24751  metdstri  24768  iccpnfcnv  24870  ovolf  25411  ovolicopnf  25453  ovolre  25454  volsup  25485  ioombl1lem4  25490  icombl1  25492  icombl  25493  ioombl  25494  uniioombllem1  25510  mbfdm  25555  ismbfd  25568  mbfmax  25578  ismbf3d  25583  itg2ge0  25664  lhop2  25948  dvfsumlem2  25961  dvfsumlem2OLD  25962  dvfsumrlim  25966  dvfsumrlim2  25967  taylfvallem1  26292  taylfval  26294  tayl0  26297  radcnvcl  26354  radcnvle  26357  psercnlem1  26363  logccv  26600  rlimcnp  26903  rlimcnp2  26904  xrlimcnp  26906  logfacbnd3  27162  chebbnd1  27411  chebbnd2  27416  dchrisumlem3  27430  log2sumbnd  27483  pntpbnd1  27525  pntibndlem2  27530  pntlemb  27536  pntleme  27547  pnt  27553  upgrfi  29071  topnfbey  30451  isblo3i  30783  xrge0infss  32747  xrdifh  32767  hashxpe  32794  elxrge02  32919  xdivpnfrp  32920  xrge0addass  33004  xrge0addgt0  33005  xrge0adddir  33006  xrge0npcan  33008  fsumrp0cl  33009  xrge0tsmsd  33049  pnfinf  33159  xrnarchi  33160  xrge0slmod  33320  unitssxrge0  33934  tpr2rico  33946  xrge0iifcnv  33967  xrge0iifiso  33969  xrge0iifhom  33971  xrge0mulc1cn  33975  pnfneige0  33985  lmxrge0  33986  esumle  34092  esumlef  34096  esumcst  34097  esumpr2  34101  esumpinfval  34107  esumpinfsum  34111  esumpcvgval  34112  hashf2  34118  esumcvg  34120  esumcvgsum  34122  voliune  34263  volfiniune  34264  ddemeas  34270  sxbrsigalem0  34305  sxbrsigalem2  34320  oms0  34331  sibfinima  34373  sitmcl  34385  probmeasb  34464  orvcgteel  34502  dstfrvclim1  34512  signsply0  34585  chtvalz  34663  hgt750lemf  34687  iooelexlt  37427  mbfposadd  37728  itg2addnclem2  37733  ftc1anclem5  37758  asindmre  37764  dvasin  37765  dvacos  37766  aks4d1p1p6  42187  readvrec2  42480  readvrec  42481  dvconstbi  44452  rfcnpre3  45155  absfico  45340  xadd0ge  45445  xrgepnfd  45455  xrge0nemnfd  45456  supxrgere  45457  supxrgelem  45461  supxrge  45462  xralrple2  45478  infxr  45490  infleinflem2  45494  xrralrecnnge  45513  infxrpnf  45569  xrpnf  45608  iocopn  45645  pnfel0pnf  45653  ge0xrre  45656  ge0lere  45657  ressiooinf  45682  uzinico  45684  uzubioo  45690  fsumge0cl  45698  limcicciooub  45760  limsupre  45764  limcresiooub  45765  limcleqr  45767  limsupresre  45819  limsupresico  45823  limsuppnfdlem  45824  limsuppnflem  45833  limsupmnflem  45843  liminfresico  45894  limsup10exlem  45895  liminflelimsuplem  45898  liminflelimsupuz  45908  limsupub2  45935  liminflbuz2  45938  liminflimsupxrre  45940  xlimpnfvlem2  45960  xlimliminflimsup  45985  icccncfext  46010  iblsplit  46089  itgsubsticclem  46098  fourierdlem31  46261  fourierdlem33  46263  fourierdlem46  46275  fourierdlem47  46276  fourierdlem48  46277  fourierdlem49  46278  fourierdlem65  46294  fourierdlem73  46302  fourierdlem75  46304  fourierdlem85  46314  fourierdlem88  46317  fourierdlem95  46324  fourierdlem97  46326  fourierdlem103  46332  fourierdlem104  46333  fourierdlem107  46336  fourierdlem109  46338  fourierdlem111  46340  fourierdlem112  46341  fourierdlem113  46342  fouriersw  46354  ioorrnopnxrlem  46429  sge0val  46489  fge0iccico  46493  gsumge0cl  46494  sge0sn  46502  sge0tsms  46503  sge0cl  46504  sge0f1o  46505  sge0ge0  46507  sge0repnf  46509  sge0fsum  46510  sge0pr  46517  sge0prle  46524  sge0split  46532  sge0p1  46537  sge0iunmptlemre  46538  sge0rpcpnf  46544  sge0rernmpt  46545  sge0isum  46550  sge0ad2en  46554  sge0xaddlem1  46556  sge0xaddlem2  46557  sge0uzfsumgt  46567  sge0seq  46569  sge0reuz  46570  voliunsge0lem  46595  meage0  46598  meassre  46600  meaiuninclem  46603  omessre  46633  omeiunltfirp  46642  carageniuncllem2  46645  carageniuncl  46646  omege0  46656  hoiprodcl  46670  hoicvrrex  46679  ovnpnfelsup  46682  ovnlerp  46685  ovnf  46686  ovn0lem  46688  ovnsubaddlem1  46693  hoiprodcl3  46703  hoidmvcl  46705  sge0hsphoire  46712  hoidmv1lelem1  46714  hoidmv1lelem2  46715  hoidmv1lelem3  46716  hoidmv1le  46717  hoidmvlelem1  46718  hoidmvlelem4  46721  hoidmvlelem5  46722  ovnhoilem1  46724  volicorege0  46760  ovolval5lem1  46775  pimgtpnf2f  46828  pimiooltgt  46833  smfliminflem  46953  rehalfge1  47460  rrxsphere  48874  itscnhlinecirc02p  48911