Theorem pnfxr 11312

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 4188	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11311	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4766	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3991	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11296	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2837	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2105   ∪ cun 3960  {cpr 4632  ℝcr 11151  +∞cpnf 11289  -∞cmnf 11290  ℝ^*cxr 11291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-pow 5370  ax-un 7753  ax-cnex 11208

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979  df-pw 4606  df-sn 4631  df-pr 4633  df-uni 4912  df-pnf 11294  df-xr 11296

This theorem is referenced by:  pnfnemnf  11313  xnn0xr  12601  xrltnr  13158  ltpnf  13159  mnfltpnf  13165  pnfnlt  13167  pnfge  13169  nltpnft  13202  xgepnf  13203  xrre  13207  xrre2  13208  xnegcl  13251  xaddf  13262  xaddpnf1  13264  xaddpnf2  13265  pnfaddmnf  13268  mnfaddpnf  13269  xaddass2  13288  xlt2add  13298  xsubge0  13299  xmulneg1  13307  xmulf  13310  xmulpnf1  13312  xmulpnf2  13313  xmulmnf1  13314  xmulpnf1n  13316  xlemul1a  13326  xadddilem  13332  xadddi2  13335  xrsupsslem  13345  xrinfmsslem  13346  supxrpnf  13356  supxrunb1  13357  supxrunb2  13358  supxrbnd  13366  xrinf0  13376  dfrp2  13432  elicore  13435  elioc2  13446  elico2  13447  elicc2  13448  ioomax  13458  iccmax  13459  ioopos  13460  elioopnf  13479  elicopnf  13481  unirnioo  13485  xrge0neqmnf  13488  elxrge0  13493  difreicc  13520  xnn0xrge0  13542  ioopnfsup  13900  icopnfsup  13901  xrsup  13904  hashbnd  14371  hashnnn0genn0  14378  hashxrcl  14392  hashdomi  14415  sgnpnf  15128  rexico  15388  limsupgre  15513  rlim3  15530  fprodge0  16025  fprodge1  16027  pcxcl  16894  pc2dvds  16912  pcadd  16922  ramxrcl  17050  ramubcl  17051  xrsnsgrp  21437  xrsdsreclblem  21447  rge0srg  21473  leordtvallem1  23233  leordtval2  23235  lecldbas  23242  pnfnei  23243  mnfnei  23244  xblpnfps  24420  xblpnf  24421  xblss2ps  24426  blssec  24460  blpnfctr  24461  nmoix  24765  icopnfcld  24803  iocmnfcld  24804  xrtgioo  24841  reconnlem1  24861  xrge0tsms  24869  metdstri  24886  iccpnfcnv  24988  ovolf  25530  ovolicopnf  25572  ovolre  25573  volsup  25604  ioombl1lem4  25609  icombl1  25611  icombl  25612  ioombl  25613  uniioombllem1  25629  mbfdm  25674  ismbfd  25687  mbfmax  25697  ismbf3d  25702  itg2ge0  25784  lhop2  26068  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumrlim  26086  dvfsumrlim2  26087  taylfvallem1  26412  taylfval  26414  tayl0  26417  radcnvcl  26474  radcnvle  26477  psercnlem1  26483  logccv  26719  rlimcnp  27022  rlimcnp2  27023  xrlimcnp  27025  logfacbnd3  27281  chebbnd1  27530  chebbnd2  27535  dchrisumlem3  27549  log2sumbnd  27602  pntpbnd1  27644  pntibndlem2  27649  pntlemb  27655  pntleme  27666  pnt  27672  upgrfi  29122  topnfbey  30497  isblo3i  30829  xrge0infss  32770  xrdifh  32788  hashxpe  32816  elxrge02  32898  xdivpnfrp  32899  xrge0addass  33003  xrge0addgt0  33004  xrge0adddir  33005  xrge0npcan  33007  fsumrp0cl  33008  xrge0tsmsd  33047  pnfinf  33172  xrnarchi  33173  xrge0slmod  33355  unitssxrge0  33860  tpr2rico  33872  xrge0iifcnv  33893  xrge0iifiso  33895  xrge0iifhom  33897  xrge0mulc1cn  33901  pnfneige0  33911  lmxrge0  33912  esumle  34038  esumlef  34042  esumcst  34043  esumpr2  34047  esumpinfval  34053  esumpinfsum  34057  esumpcvgval  34058  hashf2  34064  esumcvg  34066  esumcvgsum  34068  voliune  34209  volfiniune  34210  ddemeas  34216  sxbrsigalem0  34252  sxbrsigalem2  34267  oms0  34278  sibfinima  34320  sitmcl  34332  probmeasb  34411  orvcgteel  34448  dstfrvclim1  34458  signsply0  34544  chtvalz  34622  hgt750lemf  34646  iooelexlt  37344  mbfposadd  37653  itg2addnclem2  37658  ftc1anclem5  37683  asindmre  37689  dvasin  37690  dvacos  37691  aks4d1p1p6  42054  readvrec2  42369  readvrec  42370  dvconstbi  44329  rfcnpre3  44970  absfico  45160  xadd0ge  45270  xrgepnfd  45280  xrge0nemnfd  45281  supxrgere  45282  supxrgelem  45286  supxrge  45287  xralrple2  45303  infxr  45316  infleinflem2  45320  xrralrecnnge  45339  infxrpnf  45395  xrpnf  45435  iocopn  45472  pnfel0pnf  45480  ge0xrre  45483  ge0lere  45484  ressiooinf  45509  uzinico  45512  uzubioo  45519  fsumge0cl  45528  limcicciooub  45592  limsupre  45596  limcresiooub  45597  limcleqr  45599  limsupresre  45651  limsupresico  45655  limsuppnfdlem  45656  limsuppnflem  45665  limsupmnflem  45675  liminfresico  45726  limsup10exlem  45727  liminflelimsuplem  45730  liminflelimsupuz  45740  limsupub2  45767  liminflbuz2  45770  liminflimsupxrre  45772  xlimpnfvlem2  45792  xlimliminflimsup  45817  icccncfext  45842  iblsplit  45921  itgsubsticclem  45930  fourierdlem31  46093  fourierdlem33  46095  fourierdlem46  46107  fourierdlem47  46108  fourierdlem48  46109  fourierdlem49  46110  fourierdlem65  46126  fourierdlem73  46134  fourierdlem75  46136  fourierdlem85  46146  fourierdlem88  46149  fourierdlem95  46156  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  fourierdlem107  46168  fourierdlem109  46170  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  fouriersw  46186  ioorrnopnxrlem  46261  sge0val  46321  fge0iccico  46325  gsumge0cl  46326  sge0sn  46334  sge0tsms  46335  sge0cl  46336  sge0f1o  46337  sge0ge0  46339  sge0repnf  46341  sge0fsum  46342  sge0pr  46349  sge0prle  46356  sge0split  46364  sge0p1  46369  sge0iunmptlemre  46370  sge0rpcpnf  46376  sge0rernmpt  46377  sge0isum  46382  sge0ad2en  46386  sge0xaddlem1  46388  sge0xaddlem2  46389  sge0uzfsumgt  46399  sge0seq  46401  sge0reuz  46402  voliunsge0lem  46427  meage0  46430  meassre  46432  meaiuninclem  46435  omessre  46465  omeiunltfirp  46474  carageniuncllem2  46477  carageniuncl  46478  omege0  46488  hoiprodcl  46502  hoicvrrex  46511  ovnpnfelsup  46514  ovnlerp  46517  ovnf  46518  ovn0lem  46520  ovnsubaddlem1  46525  hoiprodcl3  46535  hoidmvcl  46537  sge0hsphoire  46544  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem4  46553  hoidmvlelem5  46554  ovnhoilem1  46556  volicorege0  46592  ovolval5lem1  46607  pimgtpnf2f  46660  pimiooltgt  46665  smfliminflem  46785  rrxsphere  48597  itscnhlinecirc02p  48634