Theorem pnfxr 11344

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 4202	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11343	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4787	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 4005	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11328	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2843	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2108   ∪ cun 3974  {cpr 4650  ℝcr 11183  +∞cpnf 11321  -∞cmnf 11322  ℝ^*cxr 11323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-pow 5383  ax-un 7770  ax-cnex 11240

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-pw 4624  df-sn 4649  df-pr 4651  df-uni 4932  df-pnf 11326  df-xr 11328

This theorem is referenced by:  pnfnemnf  11345  xnn0xr  12630  xrltnr  13182  ltpnf  13183  mnfltpnf  13189  pnfnlt  13191  pnfge  13193  nltpnft  13226  xgepnf  13227  xrre  13231  xrre2  13232  xnegcl  13275  xaddf  13286  xaddpnf1  13288  xaddpnf2  13289  pnfaddmnf  13292  mnfaddpnf  13293  xaddass2  13312  xlt2add  13322  xsubge0  13323  xmulneg1  13331  xmulf  13334  xmulpnf1  13336  xmulpnf2  13337  xmulmnf1  13338  xmulpnf1n  13340  xlemul1a  13350  xadddilem  13356  xadddi2  13359  xrsupsslem  13369  xrinfmsslem  13370  supxrpnf  13380  supxrunb1  13381  supxrunb2  13382  supxrbnd  13390  xrinf0  13400  dfrp2  13456  elicore  13459  elioc2  13470  elico2  13471  elicc2  13472  ioomax  13482  iccmax  13483  ioopos  13484  elioopnf  13503  elicopnf  13505  unirnioo  13509  xrge0neqmnf  13512  elxrge0  13517  difreicc  13544  xnn0xrge0  13566  ioopnfsup  13915  icopnfsup  13916  xrsup  13919  hashbnd  14385  hashnnn0genn0  14392  hashxrcl  14406  hashdomi  14429  sgnpnf  15142  rexico  15402  limsupgre  15527  rlim3  15544  fprodge0  16041  fprodge1  16043  pcxcl  16908  pc2dvds  16926  pcadd  16936  ramxrcl  17064  ramubcl  17065  xrsnsgrp  21443  xrsdsreclblem  21453  rge0srg  21479  leordtvallem1  23239  leordtval2  23241  lecldbas  23248  pnfnei  23249  mnfnei  23250  xblpnfps  24426  xblpnf  24427  xblss2ps  24432  blssec  24466  blpnfctr  24467  nmoix  24771  icopnfcld  24809  iocmnfcld  24810  xrtgioo  24847  reconnlem1  24867  xrge0tsms  24875  metdstri  24892  iccpnfcnv  24994  ovolf  25536  ovolicopnf  25578  ovolre  25579  volsup  25610  ioombl1lem4  25615  icombl1  25617  icombl  25618  ioombl  25619  uniioombllem1  25635  mbfdm  25680  ismbfd  25693  mbfmax  25703  ismbf3d  25708  itg2ge0  25790  lhop2  26074  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumrlim  26092  dvfsumrlim2  26093  taylfvallem1  26416  taylfval  26418  tayl0  26421  radcnvcl  26478  radcnvle  26481  psercnlem1  26487  logccv  26723  rlimcnp  27026  rlimcnp2  27027  xrlimcnp  27029  logfacbnd3  27285  chebbnd1  27534  chebbnd2  27539  dchrisumlem3  27553  log2sumbnd  27606  pntpbnd1  27648  pntibndlem2  27653  pntlemb  27659  pntleme  27670  pnt  27676  upgrfi  29126  topnfbey  30501  isblo3i  30833  xrge0infss  32767  xrdifh  32785  hashxpe  32814  elxrge02  32896  xdivpnfrp  32897  xrge0addass  33002  xrge0addgt0  33003  xrge0adddir  33004  xrge0npcan  33006  fsumrp0cl  33007  xrge0tsmsd  33041  pnfinf  33163  xrnarchi  33164  xrge0slmod  33341  unitssxrge0  33846  tpr2rico  33858  xrge0iifcnv  33879  xrge0iifiso  33881  xrge0iifhom  33883  xrge0mulc1cn  33887  pnfneige0  33897  lmxrge0  33898  esumle  34022  esumlef  34026  esumcst  34027  esumpr2  34031  esumpinfval  34037  esumpinfsum  34041  esumpcvgval  34042  hashf2  34048  esumcvg  34050  esumcvgsum  34052  voliune  34193  volfiniune  34194  ddemeas  34200  sxbrsigalem0  34236  sxbrsigalem2  34251  oms0  34262  sibfinima  34304  sitmcl  34316  probmeasb  34395  orvcgteel  34432  dstfrvclim1  34442  signsply0  34528  chtvalz  34606  hgt750lemf  34630  iooelexlt  37328  mbfposadd  37627  itg2addnclem2  37632  ftc1anclem5  37657  asindmre  37663  dvasin  37664  dvacos  37665  aks4d1p1p6  42030  dvconstbi  44303  rfcnpre3  44933  absfico  45125  xadd0ge  45235  xrgepnfd  45246  xrge0nemnfd  45247  supxrgere  45248  supxrgelem  45252  supxrge  45253  xralrple2  45269  infxr  45282  infleinflem2  45286  xrralrecnnge  45305  infxrpnf  45361  xrpnf  45401  iocopn  45438  pnfel0pnf  45446  ge0xrre  45449  ge0lere  45450  ressiooinf  45475  uzinico  45478  uzubioo  45485  fsumge0cl  45494  limcicciooub  45558  limsupre  45562  limcresiooub  45563  limcleqr  45565  limsupresre  45617  limsupresico  45621  limsuppnfdlem  45622  limsuppnflem  45631  limsupmnflem  45641  liminfresico  45692  limsup10exlem  45693  liminflelimsuplem  45696  liminflelimsupuz  45706  limsupub2  45733  liminflbuz2  45736  liminflimsupxrre  45738  xlimpnfvlem2  45758  xlimliminflimsup  45783  icccncfext  45808  iblsplit  45887  itgsubsticclem  45896  fourierdlem31  46059  fourierdlem33  46061  fourierdlem46  46073  fourierdlem47  46074  fourierdlem48  46075  fourierdlem49  46076  fourierdlem65  46092  fourierdlem73  46100  fourierdlem75  46102  fourierdlem85  46112  fourierdlem88  46115  fourierdlem95  46122  fourierdlem97  46124  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  fourierdlem109  46136  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  fouriersw  46152  ioorrnopnxrlem  46227  sge0val  46287  fge0iccico  46291  gsumge0cl  46292  sge0sn  46300  sge0tsms  46301  sge0cl  46302  sge0f1o  46303  sge0ge0  46305  sge0repnf  46307  sge0fsum  46308  sge0pr  46315  sge0prle  46322  sge0split  46330  sge0p1  46335  sge0iunmptlemre  46336  sge0rpcpnf  46342  sge0rernmpt  46343  sge0isum  46348  sge0ad2en  46352  sge0xaddlem1  46354  sge0xaddlem2  46355  sge0uzfsumgt  46365  sge0seq  46367  sge0reuz  46368  voliunsge0lem  46393  meage0  46396  meassre  46398  meaiuninclem  46401  omessre  46431  omeiunltfirp  46440  carageniuncllem2  46443  carageniuncl  46444  omege0  46454  hoiprodcl  46468  hoicvrrex  46477  ovnpnfelsup  46480  ovnlerp  46483  ovnf  46484  ovn0lem  46486  ovnsubaddlem1  46491  hoiprodcl3  46501  hoidmvcl  46503  sge0hsphoire  46510  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem4  46519  hoidmvlelem5  46520  ovnhoilem1  46522  volicorege0  46558  ovolval5lem1  46573  pimgtpnf2f  46626  pimiooltgt  46631  smfliminflem  46751  rrxsphere  48482  itscnhlinecirc02p  48519