Theorem pnfxr 11251

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 4134	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11250	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4724	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3936	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11235	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2864	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2145   ∪ cun 3905  {cpr 4587  ℝcr 11087  +∞cpnf 11228  -∞cmnf 11229  ℝ^*cxr 11230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pow 5327  ax-un 7722  ax-cnex 11144

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-pw 4560  df-sn 4586  df-pr 4588  df-uni 4869  df-pnf 11233  df-xr 11235

This theorem is referenced by:  pnfnemnf  11252  xnn0xr  12573  xrltnr  13135  ltpnf  13136  mnfltpnf  13142  pnfnlt  13144  pnfge  13146  nltpnft  13181  xgepnf  13182  xrre  13186  xrre2  13187  xnegcl  13230  xaddf  13241  xaddpnf1  13243  xaddpnf2  13244  pnfaddmnf  13247  mnfaddpnf  13248  xaddass2  13267  xlt2add  13277  xsubge0  13278  xmulneg1  13286  xmulf  13289  xmulpnf1  13291  xmulpnf2  13292  xmulmnf1  13293  xmulpnf1n  13295  xlemul1a  13305  xadddilem  13311  xadddi2  13314  xrsupsslem  13324  xrinfmsslem  13325  supxrpnf  13335  supxrunb1  13336  supxrunb2  13337  supxrbnd  13345  xrinf0  13356  dfrp2  13412  elicore  13416  elioc2  13427  elico2  13428  elicc2  13429  ioomax  13440  iccmax  13441  ioopos  13442  elioopnf  13461  elicopnf  13463  unirnioo  13467  xrge0neqmnf  13470  elxrge0  13475  difreicc  13502  xnn0xrge0  13524  ioopnfsup  13888  icopnfsup  13889  xrsup  13892  hashbnd  14363  hashnnn0genn0  14370  hashxrcl  14384  hashdomi  14407  sgnpnf  15120  rexico  15395  limsupgre  15522  rlim3  15539  fprodge0  16037  fprodge1  16039  pcxcl  16911  pc2dvds  16929  pcadd  16939  ramxrcl  17067  ramubcl  17068  xrsnsgrp  21518  xrsdsreclblem  21523  rge0srg  21548  leordtvallem1  23328  leordtval2  23330  lecldbas  23337  pnfnei  23338  mnfnei  23339  xblpnfps  24513  xblpnf  24514  xblss2ps  24519  blssec  24553  blpnfctr  24554  nmoix  24847  icopnfcld  24885  iocmnfcld  24886  xrtgioo  24925  reconnlem1  24945  xrge0tsms  24953  metdstri  24970  iccpnfcnv  25064  ovolf  25602  ovolicopnf  25644  ovolre  25645  volsup  25676  ioombl1lem4  25681  icombl1  25683  icombl  25684  ioombl  25685  uniioombllem1  25701  mbfdm  25746  ismbfd  25759  mbfmax  25769  ismbf3d  25774  itg2ge0  25855  lhop2  26135  dvfsumlem2  26147  dvfsumrlim  26151  dvfsumrlim2  26152  taylfvallem1  26478  taylfval  26480  tayl0  26483  radcnvcl  26538  radcnvle  26541  psercnlem1  26546  logccv  26786  rlimcnp  27088  rlimcnp2  27089  xrlimcnp  27091  logfacbnd3  27345  chebbnd1  27594  chebbnd2  27599  dchrisumlem3  27613  log2sumbnd  27666  pntpbnd1  27708  pntibndlem2  27713  pntlemb  27719  pntleme  27730  pnt  27736  upgrfi  29350  topnfbey  30729  isblo3i  31062  xrge0infss  33017  xrdifh  33037  hashxpe  33064  elxrge02  33164  xdivpnfrp  33165  xrge0addass  33249  xrge0addgt0  33250  xrge0adddir  33251  xrge0npcan  33253  fsumrp0cl  33254  xrge0tsmsd  33306  pnfinf  33416  xrnarchi  33417  xrge0slmod  33583  unitssxrge0  34207  tpr2rico  34219  xrge0iifcnv  34240  xrge0iifiso  34242  xrge0iifhom  34244  xrge0mulc1cn  34248  pnfneige0  34258  lmxrge0  34259  esumle  34365  esumlef  34369  esumcst  34370  esumpr2  34374  esumpinfval  34380  esumpinfsum  34384  esumpcvgval  34385  hashf2  34391  esumcvg  34393  esumcvgsum  34395  voliune  34536  volfiniune  34537  ddemeas  34543  sxbrsigalem0  34578  sxbrsigalem2  34593  oms0  34604  sibfinima  34646  sitmcl  34658  probmeasb  34737  orvcgteel  34775  dstfrvclim1  34785  signsply0  34855  chtvalz  34933  hgt750lemf  34957  iooelexlt  37868  mbfposadd  38178  itg2addnclem2  38183  ftc1anclem5  38208  asindmre  38214  dvasin  38215  dvacos  38216  aks4d1p1p6  42702  readvrec2  42982  readvrec  42983  dvconstbi  44908  rfcnpre3  45611  absfico  45792  xadd0ge  45896  xrgepnfd  45905  xrge0nemnfd  45906  supxrgere  45907  supxrgelem  45911  supxrge  45912  xralrple2  45928  infxr  45940  infleinflem2  45944  xrralrecnnge  45963  infxrpnf  46018  xrpnf  46057  iocopn  46094  pnfel0pnf  46102  ge0xrre  46105  ge0lere  46106  ressiooinf  46131  uzinico  46133  uzubioo  46139  fsumge0cl  46147  limcicciooub  46209  limsupre  46213  limcresiooub  46214  limcleqr  46216  limsupresre  46268  limsupresico  46272  limsuppnfdlem  46273  limsuppnflem  46282  limsupmnflem  46292  liminfresico  46343  limsup10exlem  46344  liminflelimsuplem  46347  liminflelimsupuz  46357  limsupub2  46384  liminflbuz2  46387  liminflimsupxrre  46389  xlimpnfvlem2  46409  xlimliminflimsup  46434  icccncfext  46459  iblsplit  46538  itgsubsticclem  46547  fourierdlem31  46710  fourierdlem33  46712  fourierdlem46  46724  fourierdlem47  46725  fourierdlem48  46726  fourierdlem49  46727  fourierdlem65  46743  fourierdlem73  46751  fourierdlem75  46753  fourierdlem85  46763  fourierdlem88  46766  fourierdlem95  46773  fourierdlem97  46775  fourierdlem103  46781  fourierdlem104  46782  fourierdlem107  46785  fourierdlem109  46787  fourierdlem111  46789  fourierdlem112  46790  fourierdlem113  46791  fouriersw  46803  ioorrnopnxrlem  46878  sge0val  46938  fge0iccico  46942  gsumge0cl  46943  sge0sn  46951  sge0tsms  46952  sge0cl  46953  sge0f1o  46954  sge0ge0  46956  sge0repnf  46958  sge0fsum  46959  sge0pr  46966  sge0prle  46973  sge0split  46981  sge0p1  46986  sge0iunmptlemre  46987  sge0rpcpnf  46993  sge0rernmpt  46994  sge0isum  46999  sge0ad2en  47003  sge0xaddlem1  47005  sge0xaddlem2  47006  sge0uzfsumgt  47016  sge0seq  47018  sge0reuz  47019  voliunsge0lem  47044  meage0  47047  meassre  47049  meaiuninclem  47052  omessre  47082  omeiunltfirp  47091  carageniuncllem2  47094  carageniuncl  47095  omege0  47105  hoiprodcl  47119  hoicvrrex  47128  ovnpnfelsup  47131  ovnlerp  47134  ovnf  47135  ovn0lem  47137  ovnsubaddlem1  47142  hoiprodcl3  47152  hoidmvcl  47154  sge0hsphoire  47161  hoidmv1lelem1  47163  hoidmv1lelem2  47164  hoidmv1lelem3  47165  hoidmv1le  47166  hoidmvlelem1  47167  hoidmvlelem4  47170  hoidmvlelem5  47171  ovnhoilem1  47173  volicorege0  47209  ovolval5lem1  47224  pimgtpnf2f  47277  pimiooltgt  47282  smfliminflem  47402  rehalfge1  47931  rrxsphere  49379  itscnhlinecirc02p  49416