Theorem pnfxr 11233

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 4131	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11232	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4720	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3933	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11217	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2860	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2141   ∪ cun 3902  {cpr 4583  ℝcr 11069  +∞cpnf 11210  -∞cmnf 11211  ℝ^*cxr 11212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pow 5321  ax-un 7714  ax-cnex 11126

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921  df-pw 4556  df-sn 4582  df-pr 4584  df-uni 4865  df-pnf 11215  df-xr 11217

This theorem is referenced by:  pnfnemnf  11234  xnn0xr  12556  xrltnr  13118  ltpnf  13119  mnfltpnf  13125  pnfnlt  13127  pnfge  13129  nltpnft  13164  xgepnf  13165  xrre  13169  xrre2  13170  xnegcl  13213  xaddf  13224  xaddpnf1  13226  xaddpnf2  13227  pnfaddmnf  13230  mnfaddpnf  13231  xaddass2  13250  xlt2add  13260  xsubge0  13261  xmulneg1  13269  xmulf  13272  xmulpnf1  13274  xmulpnf2  13275  xmulmnf1  13276  xmulpnf1n  13278  xlemul1a  13288  xadddilem  13294  xadddi2  13297  xrsupsslem  13307  xrinfmsslem  13308  supxrpnf  13318  supxrunb1  13319  supxrunb2  13320  supxrbnd  13328  xrinf0  13339  dfrp2  13395  elicore  13399  elioc2  13410  elico2  13411  elicc2  13412  ioomax  13423  iccmax  13424  ioopos  13425  elioopnf  13444  elicopnf  13446  unirnioo  13450  xrge0neqmnf  13453  elxrge0  13458  difreicc  13485  xnn0xrge0  13507  ioopnfsup  13871  icopnfsup  13872  xrsup  13875  hashbnd  14346  hashnnn0genn0  14353  hashxrcl  14367  hashdomi  14390  sgnpnf  15103  rexico  15364  limsupgre  15491  rlim3  15508  fprodge0  16006  fprodge1  16008  pcxcl  16880  pc2dvds  16898  pcadd  16908  ramxrcl  17036  ramubcl  17037  xrsnsgrp  21440  xrsdsreclblem  21445  rge0srg  21470  leordtvallem1  23250  leordtval2  23252  lecldbas  23259  pnfnei  23260  mnfnei  23261  xblpnfps  24435  xblpnf  24436  xblss2ps  24441  blssec  24475  blpnfctr  24476  nmoix  24769  icopnfcld  24807  iocmnfcld  24808  xrtgioo  24847  reconnlem1  24867  xrge0tsms  24875  metdstri  24892  iccpnfcnv  24986  ovolf  25524  ovolicopnf  25566  ovolre  25567  volsup  25598  ioombl1lem4  25603  icombl1  25605  icombl  25606  ioombl  25607  uniioombllem1  25623  mbfdm  25668  ismbfd  25681  mbfmax  25691  ismbf3d  25696  itg2ge0  25777  lhop2  26057  dvfsumlem2  26069  dvfsumrlim  26073  dvfsumrlim2  26074  taylfvallem1  26397  taylfval  26399  tayl0  26402  radcnvcl  26457  radcnvle  26460  psercnlem1  26465  logccv  26705  rlimcnp  27007  rlimcnp2  27008  xrlimcnp  27010  logfacbnd3  27264  chebbnd1  27513  chebbnd2  27518  dchrisumlem3  27532  log2sumbnd  27585  pntpbnd1  27627  pntibndlem2  27632  pntlemb  27638  pntleme  27649  pnt  27655  upgrfi  29238  topnfbey  30617  isblo3i  30950  xrge0infss  32912  xrdifh  32932  hashxpe  32959  elxrge02  33070  xdivpnfrp  33071  xrge0addass  33155  xrge0addgt0  33156  xrge0adddir  33157  xrge0npcan  33159  fsumrp0cl  33160  xrge0tsmsd  33214  pnfinf  33324  xrnarchi  33325  xrge0slmod  33495  unitssxrge0  34158  tpr2rico  34170  xrge0iifcnv  34191  xrge0iifiso  34193  xrge0iifhom  34195  xrge0mulc1cn  34199  pnfneige0  34209  lmxrge0  34210  esumle  34316  esumlef  34320  esumcst  34321  esumpr2  34325  esumpinfval  34331  esumpinfsum  34335  esumpcvgval  34336  hashf2  34342  esumcvg  34344  esumcvgsum  34346  voliune  34487  volfiniune  34488  ddemeas  34494  sxbrsigalem0  34529  sxbrsigalem2  34544  oms0  34555  sibfinima  34597  sitmcl  34609  probmeasb  34688  orvcgteel  34726  dstfrvclim1  34736  signsply0  34809  chtvalz  34887  hgt750lemf  34911  iooelexlt  37820  mbfposadd  38130  itg2addnclem2  38135  ftc1anclem5  38160  asindmre  38166  dvasin  38167  dvacos  38168  aks4d1p1p6  42654  readvrec2  42934  readvrec  42935  dvconstbi  44874  rfcnpre3  45577  absfico  45758  xadd0ge  45862  xrgepnfd  45871  xrge0nemnfd  45872  supxrgere  45873  supxrgelem  45877  supxrge  45878  xralrple2  45894  infxr  45906  infleinflem2  45910  xrralrecnnge  45929  infxrpnf  45984  xrpnf  46023  iocopn  46060  pnfel0pnf  46068  ge0xrre  46071  ge0lere  46072  ressiooinf  46097  uzinico  46099  uzubioo  46105  fsumge0cl  46113  limcicciooub  46175  limsupre  46179  limcresiooub  46180  limcleqr  46182  limsupresre  46234  limsupresico  46238  limsuppnfdlem  46239  limsuppnflem  46248  limsupmnflem  46258  liminfresico  46309  limsup10exlem  46310  liminflelimsuplem  46313  liminflelimsupuz  46323  limsupub2  46350  liminflbuz2  46353  liminflimsupxrre  46355  xlimpnfvlem2  46375  xlimliminflimsup  46400  icccncfext  46425  iblsplit  46504  itgsubsticclem  46513  fourierdlem31  46676  fourierdlem33  46678  fourierdlem46  46690  fourierdlem47  46691  fourierdlem48  46692  fourierdlem49  46693  fourierdlem65  46709  fourierdlem73  46717  fourierdlem75  46719  fourierdlem85  46729  fourierdlem88  46732  fourierdlem95  46739  fourierdlem97  46741  fourierdlem103  46747  fourierdlem104  46748  fourierdlem107  46751  fourierdlem109  46753  fourierdlem111  46755  fourierdlem112  46756  fourierdlem113  46757  fouriersw  46769  ioorrnopnxrlem  46844  sge0val  46904  fge0iccico  46908  gsumge0cl  46909  sge0sn  46917  sge0tsms  46918  sge0cl  46919  sge0f1o  46920  sge0ge0  46922  sge0repnf  46924  sge0fsum  46925  sge0pr  46932  sge0prle  46939  sge0split  46947  sge0p1  46952  sge0iunmptlemre  46953  sge0rpcpnf  46959  sge0rernmpt  46960  sge0isum  46965  sge0ad2en  46969  sge0xaddlem1  46971  sge0xaddlem2  46972  sge0uzfsumgt  46982  sge0seq  46984  sge0reuz  46985  voliunsge0lem  47010  meage0  47013  meassre  47015  meaiuninclem  47018  omessre  47048  omeiunltfirp  47057  carageniuncllem2  47060  carageniuncl  47061  omege0  47071  hoiprodcl  47085  hoicvrrex  47094  ovnpnfelsup  47097  ovnlerp  47100  ovnf  47101  ovn0lem  47103  ovnsubaddlem1  47108  hoiprodcl3  47118  hoidmvcl  47120  sge0hsphoire  47127  hoidmv1lelem1  47129  hoidmv1lelem2  47130  hoidmv1lelem3  47131  hoidmv1le  47132  hoidmvlelem1  47133  hoidmvlelem4  47136  hoidmvlelem5  47137  ovnhoilem1  47139  volicorege0  47175  ovolval5lem1  47190  pimgtpnf2f  47243  pimiooltgt  47248  smfliminflem  47368  rehalfge1  47897  rrxsphere  49334  itscnhlinecirc02p  49371