MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pnfxr Unicode version

Theorem pnfxr 10697
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  |-  +oo  e.  RR*

Proof of Theorem pnfxr
StepHypRef Expression
1 ssun2 3498 . . 3  |-  {  +oo , 
-oo }  C_  ( RR  u.  {  +oo ,  -oo } )
2 df-pnf 9106 . . . . 5  |-  +oo  =  ~P U. CC
3 cnex 9055 . . . . . . 7  |-  CC  e.  _V
43uniex 4691 . . . . . 6  |-  U. CC  e.  _V
54pwex 4369 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2500 . . . 4  |-  +oo  e.  _V
76prid1 3899 . . 3  |-  +oo  e.  { 
+oo ,  -oo }
81, 7sselii 3332 . 2  |-  +oo  e.  ( RR  u.  {  +oo , 
-oo } )
9 df-xr 9108 . 2  |-  RR*  =  ( RR  u.  {  +oo , 
-oo } )
108, 9eleqtrri 2503 1  |-  +oo  e.  RR*
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   _Vcvv 2943    u. cun 3305   ~Pcpw 3786   {cpr 3802   U.cuni 4002   CCcc 8972   RRcr 8973    +oocpnf 9101    -oocmnf 9102   RR*cxr 9103
This theorem is referenced by:  mnfxr  10698  elxr  10700  pnfnemnf  10701  xrltnr  10704  ltpnf  10705  mnfltpnf  10707  pnfnlt  10709  pnfge  10711  nltpnft  10738  xrre  10741  xrre2  10742  xnegex  10778  xnegcl  10783  xaddval  10793  xaddf  10794  xmulval  10795  xaddpnf1  10796  xaddpnf2  10797  pnfaddmnf  10800  mnfaddpnf  10801  xaddass2  10813  xlt2add  10823  xsubge0  10824  xmulneg1  10832  xmulf  10835  xmulpnf1  10837  xmulpnf2  10838  xmulmnf1  10839  xmulpnf1n  10841  xlemul1a  10851  xadddilem  10857  xadddi2  10860  xrsupsslem  10869  xrinfmsslem  10870  xrinfmss  10872  supxrpnf  10881  supxrunb1  10882  supxrunb2  10883  supxrbnd  10891  xrinfm0  10899  elioc2  10957  elico2  10958  elicc2  10959  ioomax  10969  iccmax  10970  ioopos  10971  elioopnf  10982  elicopnf  10984  unirnioo  10988  elxrge0  10992  difreicc  11012  ioopnfsup  11228  icopnfsup  11229  xrsup  11232  hashgval  11604  hashinf  11606  hashbnd  11607  hashf  11608  hashnnn0genn0  11610  hashxrcl  11623  hashdomi  11637  rexico  12140  limsupgre  12258  rlim3  12275  pcval  13201  pc0  13211  pcxcl  13217  pc2dvds  13235  pcadd  13241  ramcl2  13367  ramxrcl  13368  ramubcl  13369  abvf  15894  xrsdsreclblem  16727  rege0subm  16738  leordtvallem1  17257  leordtval2  17259  lecldbas  17266  pnfnei  17267  mnfnei  17268  xblpnfps  18408  xblpnf  18409  xblss2ps  18414  blssec  18448  blpnfctr  18449  nmoix  18746  icopnfcld  18785  iocmnfcld  18786  xrtgioo  18820  reconnlem1  18840  xrge0tsms  18848  metdstri  18864  iccpnfcnv  18952  iccpnfhmeo  18953  cphsqrcl  19130  ovolf  19361  ovollb2lem  19367  ovollb2  19368  ovolunlem1a  19375  ovolunlem1  19376  ovoliunlem1  19381  ovolicc1  19395  ovolicc2lem4  19399  ovolicopnf  19403  ovolre  19404  volsup  19433  ioombl1lem2  19436  ioombl1lem4  19438  icombl1  19440  icombl  19441  ioombl  19442  uniioombllem1  19456  uniioombllem2  19458  uniioombllem3  19460  uniioombllem6  19463  mbfdm  19503  ismbfd  19515  mbfmax  19524  ismbf3d  19529  0plef  19547  mbfi1fseqlem3  19592  mbfi1fseqlem4  19593  mbfi1fseqlem5  19594  itg2ge0  19610  itg2mulclem  19621  itg2mulc  19622  itg2monolem1  19625  itg2mono  19628  itg2i1fseq  19630  itg2gt0  19635  itg2cnlem1  19636  itg2cnlem2  19637  lhop2  19882  dvfsumlem2  19894  dvfsumrlim  19898  dvfsumrlim2  19899  taylfvallem1  20256  taylfval  20258  tayl0  20261  radcnvcl  20316  radcnvle  20319  psercnlem1  20324  logccv  20537  cxpcn3  20615  rlimcnp  20787  rlimcnp2  20788  rlimcnp3  20789  xrlimcnp  20790  efrlim  20791  jensenlem1  20808  jensenlem2  20809  amgm  20812  logfacbnd3  20990  chebbnd1  21149  chebbnd2  21154  dchrisumlem3  21168  log2sumbnd  21221  pntpbnd1  21263  pntibndlem2  21268  pntlemb  21274  pntleme  21285  pnt  21291  umgrafi  21340  sizeusglecusg  21478  vdgrf  21652  isblo3i  22285  xgepnf  24099  xrdifh  24126  elxrge02  24161  xdivpnfrp  24162  xrge0addass  24194  xrge0neqmnf  24195  xrge0addgt0  24197  xrge0adddir  24198  xrge0npcan  24199  fsumrp0cl  24200  xrge0tsmsd  24206  pnfinf  24236  xrnarchi  24237  unitssxrge0  24281  tpr2rico  24293  xrge0iifcnv  24302  xrge0iifcv  24303  xrge0iifiso  24304  xrge0iifhom  24306  xrge0mulc1cn  24310  lmlimxrge0  24317  rge0scvg  24318  pnfneige0  24319  lmxrge0  24320  lmdvg  24321  esum0  24427  esumle  24432  esumlef  24437  esumcst  24438  esumpr2  24441  esumfsupre  24444  esumpinfval  24446  esumpfinvallem  24447  esumpfinval  24448  esumpfinvalf  24449  esumpinfsum  24450  esumpcvgval  24451  esummulc1  24454  hashf2  24457  esumcvg  24459  voliune  24568  volfiniune  24569  sxbrsigalem0  24604  sxbrsigalem2  24619  sibfof  24637  sitgclg  24639  sitmcl  24646  probmeasb  24671  orvcgteel  24708  dstfrvclim1  24718  mbfposadd  26195  itg2addnclem2  26198  itg2addnclem3  26199  areacirclem4  26225  dvconstbi  27461  rfcnpre3  27613  sgnpnf  28279
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-pow 4364  ax-un 4687  ax-cnex 9030
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-rex 2698  df-v 2945  df-un 3312  df-in 3314  df-ss 3321  df-pw 3788  df-sn 3807  df-pr 3808  df-uni 4003  df-pnf 9106  df-xr 9108
  Copyright terms: Public domain W3C validator