Theorem pnfxr 11367

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 4177	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11366	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4719	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3905	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11351	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2859	1 ⊢ +∞ ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2144   ∪ cun 4149  {cpr 4586  ℝcr 11203  +∞cpnf 11344  -∞cmnf 11345  ℝ^*cxr 11346

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-un 7752  ax-cnex 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-pw 4558  df-sn 4585  df-pr 4587  df-uni 4867  df-pnf 11349  df-xr 11351

This theorem is used by:  pnfnemnf  11368  xnn0xr  12688  xrltnr  13252  ltpnf  13253  mnfltpnf  13259  pnfnlt  13261  pnfge  13263  nltpnft  13298  xgepnf  13299  xrre  13303  xrre2  13304  xnegcl  13347  xaddf  13358  xaddpnf1  13360  xaddpnf2  13361  pnfaddmnf  13364  mnfaddpnf  13365  xaddass2  13384  xlt2add  13394  xsubge0  13395  xmulneg1  13403  xmulf  13406  xmulpnf1  13408  xmulpnf2  13409  xmulmnf1  13410  xmulpnf1n  13412  xlemul1a  13422  xadddilem  13428  xadddi2  13431  xrsupsslem  13441  xrinfmsslem  13442  supxrpnf  13452  supxrunb1  13453  supxrunb2  13454  supxrbnd  13462  xrinf0  13473  dfrp2  13529  elicore  13533  elioc2  13544  elico2  13545  elicc2  13546  ioomax  13557  iccmax  13558  ioopos  13559  elioopnf  13578  elicopnf  13580  unirnioo  13584  xrge0neqmnf  13587  elxrge0  13592  difreicc  13619  xnn0xrge0  13641  ioopnfsup  14008  icopnfsup  14009  xrsup  14012  hashbnd  14484  hashnnn0genn0  14491  hashxrcl  14505  hashdomi  14528  sgnpnf  15252  rexico  15527  limsupgre  15654  rlim3  15671  fprodge0  16166  fprodge1  16168  pcxcl  17045  pc2dvds  17063  pcadd  17073  ramxrcl  17201  ramubcl  17202  xrsnsgrp  21720  xrsdsreclblem  21725  rge0srg  21750  leordtvallem1  23534  leordtval2  23536  lecldbas  23543  pnfnei  23544  mnfnei  23545  xblpnfps  24720  xblpnf  24721  xblss2ps  24726  blssec  24760  blpnfctr  24761  nmoix  25054  icopnfcld  25092  iocmnfcld  25093  xrtgioo  25132  reconnlem1  25152  xrge0tsms  25160  metdstri  25177  iccpnfcnv  25271  ovolf  25809  ovolicopnf  25851  ovolre  25852  volsup  25883  ioombl1lem4  25888  icombl1  25890  icombl  25891  ioombl  25892  uniioombllem1  25908  mbfdm  25953  ismbfd  25966  mbfmax  25976  ismbf3d  25981  itg2ge0  26062  lhop2  26341  dvfsumlem2  26353  dvfsumrlim  26357  dvfsumrlim2  26358  taylfvallem1  26690  taylfval  26692  tayl0  26695  radcnvcl  26750  radcnvle  26753  psercnlem1  26758  logccv  26997  rlimcnp  27299  rlimcnp2  27300  xrlimcnp  27302  logfacbnd3  27556  chebbnd1  27805  chebbnd2  27810  dchrisumlem3  27824  log2sumbnd  27877  pntpbnd1  27919  pntibndlem2  27924  pntlemb  27930  pntleme  27941  pnt  27947  upgrfi  29675  topnfbey  31076  isblo3i  31409  xrge0infss  33399  xrdifh  33419  hashxpe  33446  elxrge02  33545  xdivpnfrp  33546  xrge0addass  33624  xrge0addgt0  33625  xrge0adddir  33626  xrge0npcan  33628  fsumrp0cl  33629  xrge0tsmsd  33681  pnfinf  33791  xrnarchi  33792  xrge0slmod  33956  unitssxrge0  34579  tpr2rico  34591  xrge0iifcnv  34612  xrge0iifiso  34614  xrge0iifhom  34616  xrge0mulc1cn  34620  pnfneige0  34630  lmxrge0  34631  esumle  34737  esumlef  34741  esumcst  34742  esumpr2  34746  esumpinfval  34752  esumpinfsum  34756  esumpcvgval  34757  hashf2  34763  esumcvg  34765  esumcvgsum  34767  voliune  34909  volfiniune  34910  ddemeas  34916  sxbrsigalem0  34950  sxbrsigalem2  34965  oms0  34976  sibfinima  35018  sitmcl  35030  probmeasb  35109  orvcgteel  35147  dstfrvclim1  35157  signsply0  35227  chtvalz  35305  hgt750lemf  35329  iooelexlt  38379  mbfposadd  38679  itg2addnclem2  38684  ftc1anclem5  38709  asindmre  38715  dvasin  38716  dvacos  38717  aks4d1p1p6  43217  readvrec2  43506  readvrec  43507  dvconstbi  45412  rfcnpre3  46144  absfico  46325  xadd0ge  46428  xrgepnfd  46437  xrge0nemnfd  46438  supxrgere  46439  supxrgelem  46443  supxrge  46444  xralrple2  46460  infxr  46472  infleinflem2  46476  xrralrecnnge  46495  infxrpnf  46550  xrpnf  46589  iocopn  46626  pnfel0pnf  46634  ge0xrre  46637  ge0lere  46638  ressiooinf  46663  uzinico  46665  uzubioo  46671  fsumge0cl  46679  limcicciooub  46741  limsupre  46745  limcresiooub  46746  limcleqr  46748  limsupresre  46800  limsupresico  46804  limsuppnfdlem  46805  limsuppnflem  46814  limsupmnflem  46824  liminfresico  46875  limsup10exlem  46876  liminflelimsuplem  46879  liminflelimsupuz  46889  limsupub2  46916  liminflbuz2  46919  liminflimsupxrre  46921  xlimpnfvlem2  46941  xlimliminflimsup  46966  icccncfext  46991  iblsplit  47070  itgsubsticclem  47079  fourierdlem31  47242  fourierdlem33  47244  fourierdlem46  47256  fourierdlem47  47257  fourierdlem48  47258  fourierdlem49  47259  fourierdlem65  47275  fourierdlem73  47283  fourierdlem75  47285  fourierdlem85  47295  fourierdlem88  47298  fourierdlem95  47305  fourierdlem97  47307  fourierdlem103  47313  fourierdlem104  47314  fourierdlem107  47317  fourierdlem109  47319  fourierdlem111  47321  fourierdlem112  47322  fourierdlem113  47323  fouriersw  47335  ioorrnopnxrlem  47410  sge0val  47470  fge0iccico  47474  gsumge0cl  47475  sge0sn  47483  sge0tsms  47484  sge0cl  47485  sge0f1o  47486  sge0ge0  47488  sge0repnf  47490  sge0fsum  47491  sge0pr  47498  sge0prle  47505  sge0split  47513  sge0p1  47518  sge0iunmptlemre  47519  sge0rpcpnf  47525  sge0rernmpt  47526  sge0isum  47531  sge0ad2en  47535  sge0xaddlem1  47537  sge0xaddlem2  47538  sge0uzfsumgt  47548  sge0seq  47550  sge0reuz  47551  voliunsge0lem  47576  meage0  47579  meassre  47581  meaiuninclem  47584  omessre  47614  omeiunltfirp  47623  carageniuncllem2  47626  carageniuncl  47627  omege0  47637  hoiprodcl  47651  hoicvrrex  47660  ovnpnfelsup  47663  ovnlerp  47666  ovnf  47667  ovn0lem  47669  ovnsubaddlem1  47674  hoiprodcl3  47684  hoidmvcl  47686  sge0hsphoire  47693  hoidmv1lelem1  47695  hoidmv1lelem2  47696  hoidmv1lelem3  47697  hoidmv1le  47698  hoidmvlelem1  47699  hoidmvlelem4  47702  hoidmvlelem5  47703  ovnhoilem1  47705  volicorege0  47741  ovolval5lem1  47756  pimgtpnf2f  47809  pimiooltgt  47814  smfliminflem  47934  rehalfge1  48503  rrxsphere  49954  itscnhlinecirc02p  49991