Theorem pnfxr 11291

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 11290	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4726	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3931	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11275	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2861	1 ⊢ +∞ ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2145   ∪ cun 3900  {cpr 4589  ℝcr 11127  +∞cpnf 11268  -∞cmnf 11269  ℝ^*cxr 11270

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pow 5334  ax-un 7740  ax-cnex 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-pw 4562  df-sn 4588  df-pr 4590  df-uni 4871  df-pnf 11273  df-xr 11275

This theorem is used by:  pnfnemnf  11292  xnn0xr  12610  xrltnr  13174  ltpnf  13175  mnfltpnf  13181  pnfnlt  13183  pnfge  13185  nltpnft  13220  xgepnf  13221  xrre  13225  xrre2  13226  xnegcl  13269  xaddf  13280  xaddpnf1  13282  xaddpnf2  13283  pnfaddmnf  13286  mnfaddpnf  13287  xaddass2  13306  xlt2add  13316  xsubge0  13317  xmulneg1  13325  xmulf  13328  xmulpnf1  13330  xmulpnf2  13331  xmulmnf1  13332  xmulpnf1n  13334  xlemul1a  13344  xadddilem  13350  xadddi2  13353  xrsupsslem  13363  xrinfmsslem  13364  supxrpnf  13374  supxrunb1  13375  supxrunb2  13376  supxrbnd  13384  xrinf0  13395  dfrp2  13451  elicore  13455  elioc2  13466  elico2  13467  elicc2  13468  ioomax  13479  iccmax  13480  ioopos  13481  elioopnf  13500  elicopnf  13502  unirnioo  13506  xrge0neqmnf  13509  elxrge0  13514  difreicc  13541  xnn0xrge0  13563  ioopnfsup  13929  icopnfsup  13930  xrsup  13933  hashbnd  14404  hashnnn0genn0  14411  hashxrcl  14425  hashdomi  14448  sgnpnf  15170  rexico  15445  limsupgre  15572  rlim3  15589  fprodge0  16086  fprodge1  16088  pcxcl  16959  pc2dvds  16977  pcadd  16987  ramxrcl  17115  ramubcl  17116  xrsnsgrp  21627  xrsdsreclblem  21632  rge0srg  21657  leordtvallem1  23441  leordtval2  23443  lecldbas  23450  pnfnei  23451  mnfnei  23452  xblpnfps  24627  xblpnf  24628  xblss2ps  24633  blssec  24667  blpnfctr  24668  nmoix  24961  icopnfcld  24999  iocmnfcld  25000  xrtgioo  25039  reconnlem1  25059  xrge0tsms  25067  metdstri  25084  iccpnfcnv  25178  ovolf  25716  ovolicopnf  25758  ovolre  25759  volsup  25790  ioombl1lem4  25795  icombl1  25797  icombl  25798  ioombl  25799  uniioombllem1  25815  mbfdm  25860  ismbfd  25873  mbfmax  25883  ismbf3d  25888  itg2ge0  25969  lhop2  26249  dvfsumlem2  26261  dvfsumrlim  26265  dvfsumrlim2  26266  taylfvallem1  26600  taylfval  26602  tayl0  26605  radcnvcl  26660  radcnvle  26663  psercnlem1  26668  logccv  26908  rlimcnp  27210  rlimcnp2  27211  xrlimcnp  27213  logfacbnd3  27467  chebbnd1  27716  chebbnd2  27721  dchrisumlem3  27735  log2sumbnd  27788  pntpbnd1  27830  pntibndlem2  27835  pntlemb  27841  pntleme  27852  pnt  27858  upgrfi  29556  topnfbey  30957  isblo3i  31290  xrge0infss  33239  xrdifh  33259  hashxpe  33286  elxrge02  33385  xdivpnfrp  33386  xrge0addass  33464  xrge0addgt0  33465  xrge0adddir  33466  xrge0npcan  33468  fsumrp0cl  33469  xrge0tsmsd  33521  pnfinf  33631  xrnarchi  33632  xrge0slmod  33796  unitssxrge0  34418  tpr2rico  34430  xrge0iifcnv  34451  xrge0iifiso  34453  xrge0iifhom  34455  xrge0mulc1cn  34459  pnfneige0  34469  lmxrge0  34470  esumle  34576  esumlef  34580  esumcst  34581  esumpr2  34585  esumpinfval  34591  esumpinfsum  34595  esumpcvgval  34596  hashf2  34602  esumcvg  34604  esumcvgsum  34606  voliune  34748  volfiniune  34749  ddemeas  34755  sxbrsigalem0  34790  sxbrsigalem2  34805  oms0  34816  sibfinima  34858  sitmcl  34870  probmeasb  34949  orvcgteel  34987  dstfrvclim1  34997  signsply0  35067  chtvalz  35145  hgt750lemf  35169  iooelexlt  38124  mbfposadd  38424  itg2addnclem2  38429  ftc1anclem5  38454  asindmre  38460  dvasin  38461  dvacos  38462  aks4d1p1p6  42947  readvrec2  43244  readvrec  43245  dvconstbi  45166  rfcnpre3  45875  absfico  46056  xadd0ge  46160  xrgepnfd  46169  xrge0nemnfd  46170  supxrgere  46171  supxrgelem  46175  supxrge  46176  xralrple2  46192  infxr  46204  infleinflem2  46208  xrralrecnnge  46227  infxrpnf  46282  xrpnf  46321  iocopn  46358  pnfel0pnf  46366  ge0xrre  46369  ge0lere  46370  ressiooinf  46395  uzinico  46397  uzubioo  46403  fsumge0cl  46411  limcicciooub  46473  limsupre  46477  limcresiooub  46478  limcleqr  46480  limsupresre  46532  limsupresico  46536  limsuppnfdlem  46537  limsuppnflem  46546  limsupmnflem  46556  liminfresico  46607  limsup10exlem  46608  liminflelimsuplem  46611  liminflelimsupuz  46621  limsupub2  46648  liminflbuz2  46651  liminflimsupxrre  46653  xlimpnfvlem2  46673  xlimliminflimsup  46698  icccncfext  46723  iblsplit  46802  itgsubsticclem  46811  fourierdlem31  46974  fourierdlem33  46976  fourierdlem46  46988  fourierdlem47  46989  fourierdlem48  46990  fourierdlem49  46991  fourierdlem65  47007  fourierdlem73  47015  fourierdlem75  47017  fourierdlem85  47027  fourierdlem88  47030  fourierdlem95  47037  fourierdlem97  47039  fourierdlem103  47045  fourierdlem104  47046  fourierdlem107  47049  fourierdlem109  47051  fourierdlem111  47053  fourierdlem112  47054  fourierdlem113  47055  fouriersw  47067  ioorrnopnxrlem  47142  sge0val  47202  fge0iccico  47206  gsumge0cl  47207  sge0sn  47215  sge0tsms  47216  sge0cl  47217  sge0f1o  47218  sge0ge0  47220  sge0repnf  47222  sge0fsum  47223  sge0pr  47230  sge0prle  47237  sge0split  47245  sge0p1  47250  sge0iunmptlemre  47251  sge0rpcpnf  47257  sge0rernmpt  47258  sge0isum  47263  sge0ad2en  47267  sge0xaddlem1  47269  sge0xaddlem2  47270  sge0uzfsumgt  47280  sge0seq  47282  sge0reuz  47283  voliunsge0lem  47308  meage0  47311  meassre  47313  meaiuninclem  47316  omessre  47346  omeiunltfirp  47355  carageniuncllem2  47358  carageniuncl  47359  omege0  47369  hoiprodcl  47383  hoicvrrex  47392  ovnpnfelsup  47395  ovnlerp  47398  ovnf  47399  ovn0lem  47401  ovnsubaddlem1  47406  hoiprodcl3  47416  hoidmvcl  47418  sge0hsphoire  47425  hoidmv1lelem1  47427  hoidmv1lelem2  47428  hoidmv1lelem3  47429  hoidmv1le  47430  hoidmvlelem1  47431  hoidmvlelem4  47434  hoidmvlelem5  47435  ovnhoilem1  47437  volicorege0  47473  ovolval5lem1  47488  pimgtpnf2f  47541  pimiooltgt  47546  smfliminflem  47666  rehalfge1  48235  rrxsphere  49686  itscnhlinecirc02p  49723