Theorem pnfxr 10092

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 3777	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		df-pnf 10076	. . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ
3		cnex 10017	. . . . . . 7 ⊢ ℂ ∈ V
4	3	uniex 6953	. . . . . 6 ⊢ ∪ ℂ ∈ V
5	4	pwex 4848	. . . . 5 ⊢ 𝒫 ∪ ℂ ∈ V
6	2, 5	eqeltri 2697	. . . 4 ⊢ +∞ ∈ V
7	6	prid1 4297	. . 3 ⊢ +∞ ∈ {+∞, -∞}
8	1, 7	sselii 3600	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
9		df-xr 10078	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
10	8, 9	eleqtrri 2700	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 1990  Vcvv 3200   ∪ cun 3572  𝒫 cpw 4158  {cpr 4179  ∪ cuni 4436  ℂcc 9934  ℝcr 9935  +∞cpnf 10071  -∞cmnf 10072  ℝ^*cxr 10073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-pow 4843  ax-un 6949  ax-cnex 9992

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-pw 4160  df-sn 4178  df-pr 4180  df-uni 4437  df-pnf 10076  df-xr 10078

This theorem is referenced by:  pnfex  10093  pnfnemnf  10094  xnn0xr  11368  xrltnr  11953  ltpnf  11954  mnfltpnf  11960  pnfnlt  11962  pnfge  11964  nltpnft  11995  xgepnf  11996  xrre  12000  xrre2  12001  xnegcl  12044  xaddf  12055  xaddpnf1  12057  xaddpnf2  12058  pnfaddmnf  12061  mnfaddpnf  12062  xaddass2  12080  xlt2add  12090  xsubge0  12091  xmulneg1  12099  xmulf  12102  xmulpnf1  12104  xmulpnf2  12105  xmulmnf1  12106  xmulpnf1n  12108  xlemul1a  12118  xadddilem  12124  xadddi2  12127  xrsupsslem  12137  xrinfmsslem  12138  supxrpnf  12148  supxrunb1  12149  supxrunb2  12150  supxrbnd  12158  xrinf0  12168  elicore  12226  elioc2  12236  elico2  12237  elicc2  12238  ioomax  12248  iccmax  12249  ioopos  12250  elioopnf  12267  elicopnf  12269  unirnioo  12273  xrge0neqmnf  12276  elxrge0  12281  difreicc  12304  xnn0xrge0  12325  ioopnfsup  12663  icopnfsup  12664  xrsup  12667  hashbnd  13123  hashnnn0genn0  13131  hashxrcl  13148  hashdomi  13169  sgnpnf  13833  rexico  14093  limsupgre  14212  rlim3  14229  fprodge0  14724  fprodge1  14726  pcxcl  15565  pc2dvds  15583  pcadd  15593  ramxrcl  15721  ramubcl  15722  xrsnsgrp  19782  xrsdsreclblem  19792  rge0srg  19817  leordtvallem1  21014  leordtval2  21016  lecldbas  21023  pnfnei  21024  mnfnei  21025  xblpnfps  22200  xblpnf  22201  xblss2ps  22206  blssec  22240  blpnfctr  22241  nmoix  22533  icopnfcld  22571  iocmnfcld  22572  xrtgioo  22609  reconnlem1  22629  xrge0tsms  22637  metdstri  22654  iccpnfcnv  22743  ovolf  23250  ovolicopnf  23292  ovolre  23293  volsup  23324  ioombl1lem4  23329  icombl1  23331  icombl  23332  ioombl  23333  uniioombllem1  23349  mbfdm  23395  ismbfd  23407  mbfmax  23416  ismbf3d  23421  itg2ge0  23502  lhop2  23778  dvfsumlem2  23790  dvfsumrlim  23794  dvfsumrlim2  23795  taylfvallem1  24111  taylfval  24113  tayl0  24116  radcnvcl  24171  radcnvle  24174  psercnlem1  24179  logccv  24409  rlimcnp  24692  rlimcnp2  24693  xrlimcnp  24695  logfacbnd3  24948  chebbnd1  25161  chebbnd2  25166  dchrisumlem3  25180  log2sumbnd  25233  pntpbnd1  25275  pntibndlem2  25280  pntlemb  25286  pntleme  25297  pnt  25303  upgrfi  25986  topnfbey  27325  isblo3i  27656  xrge0infss  29525  dfrp2  29532  xrdifh  29542  elxrge02  29640  xdivpnfrp  29641  xrge0addass  29690  xrge0addgt0  29691  xrge0adddir  29692  xrge0npcan  29694  fsumrp0cl  29695  pnfinf  29737  xrnarchi  29738  xrge0tsmsd  29785  xrge0slmod  29844  unitssxrge0  29946  tpr2rico  29958  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhom  29983  xrge0mulc1cn  29987  pnfneige0  29997  lmxrge0  29998  esumle  30120  esumlef  30124  esumcst  30125  esumpr2  30129  esumpinfval  30135  esumpinfsum  30139  esumpcvgval  30140  hashf2  30146  esumcvg  30148  esumcvgsum  30150  voliune  30292  volfiniune  30293  ddemeas  30299  sxbrsigalem0  30333  sxbrsigalem2  30348  oms0  30359  sibfinima  30401  sitmcl  30413  probmeasb  30492  orvcgteel  30529  dstfrvclim1  30539  signsply0  30628  chtvalz  30707  hgt750lemf  30731  iooelexlt  33210  mbfposadd  33457  itg2addnclem2  33462  ftc1anclem5  33489  asindmre  33495  dvasin  33496  dvacos  33497  dvconstbi  38533  rfcnpre3  39192  absfico  39410  xadd0ge  39536  xrgepnfd  39547  xrge0nemnfd  39548  supxrgere  39549  supxrgelem  39553  supxrge  39554  xralrple2  39570  infxr  39583  infleinflem2  39587  xrralrecnnge  39613  infxrpnf  39674  iocopn  39746  pnfel0pnf  39754  ge0nemnf2  39755  ge0xrre  39758  ge0lere  39759  ressiooinf  39784  uzinico  39787  uzubioo  39794  fsumge0cl  39805  limcicciooub  39869  limsupre  39873  limcresiooub  39874  limcleqr  39876  limsupresre  39928  limsupresico  39932  limsuppnfdlem  39933  limsuppnflem  39942  limsupmnflem  39952  liminfresico  40003  limsup10exlem  40004  liminflelimsuplem  40007  liminflelimsupuz  40017  xlimpnfvlem2  40063  icccncfext  40100  iblsplit  40182  itgsubsticclem  40191  fourierdlem31  40355  fourierdlem33  40357  fourierdlem46  40369  fourierdlem47  40370  fourierdlem48  40371  fourierdlem49  40372  fourierdlem65  40388  fourierdlem73  40396  fourierdlem75  40398  fourierdlem85  40408  fourierdlem88  40411  fourierdlem95  40418  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  fourierdlem107  40430  fourierdlem109  40432  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  fouriersw  40448  ioorrnopnxrlem  40526  sge0val  40583  fge0iccico  40587  gsumge0cl  40588  sge0sn  40596  sge0tsms  40597  sge0cl  40598  sge0f1o  40599  sge0ge0  40601  sge0repnf  40603  sge0fsum  40604  sge0pr  40611  sge0prle  40618  sge0split  40626  sge0p1  40631  sge0iunmptlemre  40632  sge0rpcpnf  40638  sge0rernmpt  40639  sge0isum  40644  sge0ad2en  40648  sge0xaddlem1  40650  sge0xaddlem2  40651  sge0uzfsumgt  40661  sge0seq  40663  sge0reuz  40664  voliunsge0lem  40689  meage0  40692  meassre  40694  meaiuninclem  40697  omessre  40724  omeiunltfirp  40733  carageniuncllem2  40736  carageniuncl  40737  omege0  40747  hoiprodcl  40761  hoicvrrex  40770  ovnpnfelsup  40773  ovnlerp  40776  ovnf  40777  ovn0lem  40779  ovnsubaddlem1  40784  hoiprodcl3  40794  hoidmvcl  40796  sge0hsphoire  40803  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem4  40812  hoidmvlelem5  40813  ovnhoilem1  40815  volicorege0  40851  ovolval5lem1  40866  pimgtpnf2  40917  pimiooltgt  40921  smfliminflem  41036