Theorem pnfxr 11268

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 4174	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11267	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4767	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3980	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11252	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2833	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2107   ∪ cun 3947  {cpr 4631  ℝcr 11109  +∞cpnf 11245  -∞cmnf 11246  ℝ^*cxr 11247

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 2704  ax-sep 5300  ax-pow 5364  ax-un 7725  ax-cnex 11166

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-pw 4605  df-sn 4630  df-pr 4632  df-uni 4910  df-pnf 11250  df-xr 11252

This theorem is referenced by:  pnfnemnf  11269  xnn0xr  12549  xrltnr  13099  ltpnf  13100  mnfltpnf  13106  pnfnlt  13108  pnfge  13110  nltpnft  13143  xgepnf  13144  xrre  13148  xrre2  13149  xnegcl  13192  xaddf  13203  xaddpnf1  13205  xaddpnf2  13206  pnfaddmnf  13209  mnfaddpnf  13210  xaddass2  13229  xlt2add  13239  xsubge0  13240  xmulneg1  13248  xmulf  13251  xmulpnf1  13253  xmulpnf2  13254  xmulmnf1  13255  xmulpnf1n  13257  xlemul1a  13267  xadddilem  13273  xadddi2  13276  xrsupsslem  13286  xrinfmsslem  13287  supxrpnf  13297  supxrunb1  13298  supxrunb2  13299  supxrbnd  13307  xrinf0  13317  dfrp2  13373  elicore  13376  elioc2  13387  elico2  13388  elicc2  13389  ioomax  13399  iccmax  13400  ioopos  13401  elioopnf  13420  elicopnf  13422  unirnioo  13426  xrge0neqmnf  13429  elxrge0  13434  difreicc  13461  xnn0xrge0  13483  ioopnfsup  13829  icopnfsup  13830  xrsup  13833  hashbnd  14296  hashnnn0genn0  14303  hashxrcl  14317  hashdomi  14340  sgnpnf  15040  rexico  15300  limsupgre  15425  rlim3  15442  fprodge0  15937  fprodge1  15939  pcxcl  16794  pc2dvds  16812  pcadd  16822  ramxrcl  16950  ramubcl  16951  xrsnsgrp  20981  xrsdsreclblem  20991  rge0srg  21016  leordtvallem1  22714  leordtval2  22716  lecldbas  22723  pnfnei  22724  mnfnei  22725  xblpnfps  23901  xblpnf  23902  xblss2ps  23907  blssec  23941  blpnfctr  23942  nmoix  24246  icopnfcld  24284  iocmnfcld  24285  xrtgioo  24322  reconnlem1  24342  xrge0tsms  24350  metdstri  24367  iccpnfcnv  24460  ovolf  24999  ovolicopnf  25041  ovolre  25042  volsup  25073  ioombl1lem4  25078  icombl1  25080  icombl  25081  ioombl  25082  uniioombllem1  25098  mbfdm  25143  ismbfd  25156  mbfmax  25166  ismbf3d  25171  itg2ge0  25253  lhop2  25532  dvfsumlem2  25544  dvfsumrlim  25548  dvfsumrlim2  25549  taylfvallem1  25869  taylfval  25871  tayl0  25874  radcnvcl  25929  radcnvle  25932  psercnlem1  25937  logccv  26171  rlimcnp  26470  rlimcnp2  26471  xrlimcnp  26473  logfacbnd3  26726  chebbnd1  26975  chebbnd2  26980  dchrisumlem3  26994  log2sumbnd  27047  pntpbnd1  27089  pntibndlem2  27094  pntlemb  27100  pntleme  27111  pnt  27117  upgrfi  28351  topnfbey  29722  isblo3i  30054  xrge0infss  31973  xrdifh  31991  hashxpe  32019  elxrge02  32098  xdivpnfrp  32099  xrge0addass  32191  xrge0addgt0  32192  xrge0adddir  32193  xrge0npcan  32195  fsumrp0cl  32196  xrge0tsmsd  32209  pnfinf  32329  xrnarchi  32330  xrge0slmod  32463  unitssxrge0  32880  tpr2rico  32892  xrge0iifcnv  32913  xrge0iifiso  32915  xrge0iifhom  32917  xrge0mulc1cn  32921  pnfneige0  32931  lmxrge0  32932  esumle  33056  esumlef  33060  esumcst  33061  esumpr2  33065  esumpinfval  33071  esumpinfsum  33075  esumpcvgval  33076  hashf2  33082  esumcvg  33084  esumcvgsum  33086  voliune  33227  volfiniune  33228  ddemeas  33234  sxbrsigalem0  33270  sxbrsigalem2  33285  oms0  33296  sibfinima  33338  sitmcl  33350  probmeasb  33429  orvcgteel  33466  dstfrvclim1  33476  signsply0  33562  chtvalz  33641  hgt750lemf  33665  gg-dvfsumlem2  35183  iooelexlt  36243  mbfposadd  36535  itg2addnclem2  36540  ftc1anclem5  36565  asindmre  36571  dvasin  36572  dvacos  36573  aks4d1p1p6  40938  dvconstbi  43093  rfcnpre3  43717  absfico  43917  xadd0ge  44030  xrgepnfd  44041  xrge0nemnfd  44042  supxrgere  44043  supxrgelem  44047  supxrge  44048  xralrple2  44064  infxr  44077  infleinflem2  44081  xrralrecnnge  44100  infxrpnf  44156  xrpnf  44196  iocopn  44233  pnfel0pnf  44241  ge0xrre  44244  ge0lere  44245  ressiooinf  44270  uzinico  44273  uzubioo  44280  fsumge0cl  44289  limcicciooub  44353  limsupre  44357  limcresiooub  44358  limcleqr  44360  limsupresre  44412  limsupresico  44416  limsuppnfdlem  44417  limsuppnflem  44426  limsupmnflem  44436  liminfresico  44487  limsup10exlem  44488  liminflelimsuplem  44491  liminflelimsupuz  44501  limsupub2  44528  liminflbuz2  44531  liminflimsupxrre  44533  xlimpnfvlem2  44553  xlimliminflimsup  44578  icccncfext  44603  iblsplit  44682  itgsubsticclem  44691  fourierdlem31  44854  fourierdlem33  44856  fourierdlem46  44868  fourierdlem47  44869  fourierdlem48  44870  fourierdlem49  44871  fourierdlem65  44887  fourierdlem73  44895  fourierdlem75  44897  fourierdlem85  44907  fourierdlem88  44910  fourierdlem95  44917  fourierdlem97  44919  fourierdlem103  44925  fourierdlem104  44926  fourierdlem107  44929  fourierdlem109  44931  fourierdlem111  44933  fourierdlem112  44934  fourierdlem113  44935  fouriersw  44947  ioorrnopnxrlem  45022  sge0val  45082  fge0iccico  45086  gsumge0cl  45087  sge0sn  45095  sge0tsms  45096  sge0cl  45097  sge0f1o  45098  sge0ge0  45100  sge0repnf  45102  sge0fsum  45103  sge0pr  45110  sge0prle  45117  sge0split  45125  sge0p1  45130  sge0iunmptlemre  45131  sge0rpcpnf  45137  sge0rernmpt  45138  sge0isum  45143  sge0ad2en  45147  sge0xaddlem1  45149  sge0xaddlem2  45150  sge0uzfsumgt  45160  sge0seq  45162  sge0reuz  45163  voliunsge0lem  45188  meage0  45191  meassre  45193  meaiuninclem  45196  omessre  45226  omeiunltfirp  45235  carageniuncllem2  45238  carageniuncl  45239  omege0  45249  hoiprodcl  45263  hoicvrrex  45272  ovnpnfelsup  45275  ovnlerp  45278  ovnf  45279  ovn0lem  45281  ovnsubaddlem1  45286  hoiprodcl3  45296  hoidmvcl  45298  sge0hsphoire  45305  hoidmv1lelem1  45307  hoidmv1lelem2  45308  hoidmv1lelem3  45309  hoidmv1le  45310  hoidmvlelem1  45311  hoidmvlelem4  45314  hoidmvlelem5  45315  ovnhoilem1  45317  volicorege0  45353  ovolval5lem1  45368  pimgtpnf2f  45421  pimiooltgt  45426  smfliminflem  45546  rrxsphere  47434  itscnhlinecirc02p  47471