Theorem pnfxr 11190

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 4120	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11189	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4707	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3919	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11174	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2836	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2114   ∪ cun 3888  {cpr 4570  ℝcr 11028  +∞cpnf 11167  -∞cmnf 11168  ℝ^*cxr 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-un 7682  ax-cnex 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-pw 4544  df-sn 4569  df-pr 4571  df-uni 4852  df-pnf 11172  df-xr 11174

This theorem is referenced by:  pnfnemnf  11191  xnn0xr  12506  xrltnr  13061  ltpnf  13062  mnfltpnf  13068  pnfnlt  13070  pnfge  13072  nltpnft  13107  xgepnf  13108  xrre  13112  xrre2  13113  xnegcl  13156  xaddf  13167  xaddpnf1  13169  xaddpnf2  13170  pnfaddmnf  13173  mnfaddpnf  13174  xaddass2  13193  xlt2add  13203  xsubge0  13204  xmulneg1  13212  xmulf  13215  xmulpnf1  13217  xmulpnf2  13218  xmulmnf1  13219  xmulpnf1n  13221  xlemul1a  13231  xadddilem  13237  xadddi2  13240  xrsupsslem  13250  xrinfmsslem  13251  supxrpnf  13261  supxrunb1  13262  supxrunb2  13263  supxrbnd  13271  xrinf0  13282  dfrp2  13338  elicore  13342  elioc2  13353  elico2  13354  elicc2  13355  ioomax  13366  iccmax  13367  ioopos  13368  elioopnf  13387  elicopnf  13389  unirnioo  13393  xrge0neqmnf  13396  elxrge0  13401  difreicc  13428  xnn0xrge0  13450  ioopnfsup  13814  icopnfsup  13815  xrsup  13818  hashbnd  14289  hashnnn0genn0  14296  hashxrcl  14310  hashdomi  14333  sgnpnf  15046  rexico  15307  limsupgre  15434  rlim3  15451  fprodge0  15949  fprodge1  15951  pcxcl  16823  pc2dvds  16841  pcadd  16851  ramxrcl  16979  ramubcl  16980  xrsnsgrp  21397  xrsdsreclblem  21402  rge0srg  21428  leordtvallem1  23185  leordtval2  23187  lecldbas  23194  pnfnei  23195  mnfnei  23196  xblpnfps  24370  xblpnf  24371  xblss2ps  24376  blssec  24410  blpnfctr  24411  nmoix  24704  icopnfcld  24742  iocmnfcld  24743  xrtgioo  24782  reconnlem1  24802  xrge0tsms  24810  metdstri  24827  iccpnfcnv  24921  ovolf  25459  ovolicopnf  25501  ovolre  25502  volsup  25533  ioombl1lem4  25538  icombl1  25540  icombl  25541  ioombl  25542  uniioombllem1  25558  mbfdm  25603  ismbfd  25616  mbfmax  25626  ismbf3d  25631  itg2ge0  25712  lhop2  25992  dvfsumlem2  26004  dvfsumrlim  26008  dvfsumrlim2  26009  taylfvallem1  26333  taylfval  26335  tayl0  26338  radcnvcl  26395  radcnvle  26398  psercnlem1  26403  logccv  26640  rlimcnp  26942  rlimcnp2  26943  xrlimcnp  26945  logfacbnd3  27200  chebbnd1  27449  chebbnd2  27454  dchrisumlem3  27468  log2sumbnd  27521  pntpbnd1  27563  pntibndlem2  27568  pntlemb  27574  pntleme  27585  pnt  27591  upgrfi  29174  topnfbey  30554  isblo3i  30887  xrge0infss  32848  xrdifh  32868  hashxpe  32895  elxrge02  33006  xdivpnfrp  33007  xrge0addass  33091  xrge0addgt0  33092  xrge0adddir  33093  xrge0npcan  33095  fsumrp0cl  33096  xrge0tsmsd  33149  pnfinf  33259  xrnarchi  33260  xrge0slmod  33423  unitssxrge0  34060  tpr2rico  34072  xrge0iifcnv  34093  xrge0iifiso  34095  xrge0iifhom  34097  xrge0mulc1cn  34101  pnfneige0  34111  lmxrge0  34112  esumle  34218  esumlef  34222  esumcst  34223  esumpr2  34227  esumpinfval  34233  esumpinfsum  34237  esumpcvgval  34238  hashf2  34244  esumcvg  34246  esumcvgsum  34248  voliune  34389  volfiniune  34390  ddemeas  34396  sxbrsigalem0  34431  sxbrsigalem2  34446  oms0  34457  sibfinima  34499  sitmcl  34511  probmeasb  34590  orvcgteel  34628  dstfrvclim1  34638  signsply0  34711  chtvalz  34789  hgt750lemf  34813  iooelexlt  37692  mbfposadd  38002  itg2addnclem2  38007  ftc1anclem5  38032  asindmre  38038  dvasin  38039  dvacos  38040  aks4d1p1p6  42526  readvrec2  42807  readvrec  42808  dvconstbi  44779  rfcnpre3  45482  absfico  45665  xadd0ge  45770  xrgepnfd  45779  xrge0nemnfd  45780  supxrgere  45781  supxrgelem  45785  supxrge  45786  xralrple2  45802  infxr  45814  infleinflem2  45818  xrralrecnnge  45837  infxrpnf  45892  xrpnf  45931  iocopn  45968  pnfel0pnf  45976  ge0xrre  45979  ge0lere  45980  ressiooinf  46005  uzinico  46007  uzubioo  46013  fsumge0cl  46021  limcicciooub  46083  limsupre  46087  limcresiooub  46088  limcleqr  46090  limsupresre  46142  limsupresico  46146  limsuppnfdlem  46147  limsuppnflem  46156  limsupmnflem  46166  liminfresico  46217  limsup10exlem  46218  liminflelimsuplem  46221  liminflelimsupuz  46231  limsupub2  46258  liminflbuz2  46261  liminflimsupxrre  46263  xlimpnfvlem2  46283  xlimliminflimsup  46308  icccncfext  46333  iblsplit  46412  itgsubsticclem  46421  fourierdlem31  46584  fourierdlem33  46586  fourierdlem46  46598  fourierdlem47  46599  fourierdlem48  46600  fourierdlem49  46601  fourierdlem65  46617  fourierdlem73  46625  fourierdlem75  46627  fourierdlem85  46637  fourierdlem88  46640  fourierdlem95  46647  fourierdlem97  46649  fourierdlem103  46655  fourierdlem104  46656  fourierdlem107  46659  fourierdlem109  46661  fourierdlem111  46663  fourierdlem112  46664  fourierdlem113  46665  fouriersw  46677  ioorrnopnxrlem  46752  sge0val  46812  fge0iccico  46816  gsumge0cl  46817  sge0sn  46825  sge0tsms  46826  sge0cl  46827  sge0f1o  46828  sge0ge0  46830  sge0repnf  46832  sge0fsum  46833  sge0pr  46840  sge0prle  46847  sge0split  46855  sge0p1  46860  sge0iunmptlemre  46861  sge0rpcpnf  46867  sge0rernmpt  46868  sge0isum  46873  sge0ad2en  46877  sge0xaddlem1  46879  sge0xaddlem2  46880  sge0uzfsumgt  46890  sge0seq  46892  sge0reuz  46893  voliunsge0lem  46918  meage0  46921  meassre  46923  meaiuninclem  46926  omessre  46956  omeiunltfirp  46965  carageniuncllem2  46968  carageniuncl  46969  omege0  46979  hoiprodcl  46993  hoicvrrex  47002  ovnpnfelsup  47005  ovnlerp  47008  ovnf  47009  ovn0lem  47011  ovnsubaddlem1  47016  hoiprodcl3  47026  hoidmvcl  47028  sge0hsphoire  47035  hoidmv1lelem1  47037  hoidmv1lelem2  47038  hoidmv1lelem3  47039  hoidmv1le  47040  hoidmvlelem1  47041  hoidmvlelem4  47044  hoidmvlelem5  47045  ovnhoilem1  47047  volicorege0  47083  ovolval5lem1  47098  pimgtpnf2f  47151  pimiooltgt  47156  smfliminflem  47276  rehalfge1  47799  rrxsphere  49236  itscnhlinecirc02p  49273