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

Theorem pnfxr 10471
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 3352 . . 3  |-  {  +oo , 
-oo }  C_  ( RR  u.  {  +oo ,  -oo } )
2 df-pnf 8885 . . . . 5  |-  +oo  =  ~P U. CC
3 cnex 8834 . . . . . . 7  |-  CC  e.  _V
43uniex 4532 . . . . . 6  |-  U. CC  e.  _V
54pwex 4209 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2366 . . . 4  |-  +oo  e.  _V
76prid1 3747 . . 3  |-  +oo  e.  { 
+oo ,  -oo }
81, 7sselii 3190 . 2  |-  +oo  e.  ( RR  u.  {  +oo , 
-oo } )
9 df-xr 8887 . 2  |-  RR*  =  ( RR  u.  {  +oo , 
-oo } )
108, 9eleqtrri 2369 1  |-  +oo  e.  RR*
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801    u. cun 3163   ~Pcpw 3638   {cpr 3654   U.cuni 3843   CCcc 8751   RRcr 8752    +oocpnf 8880    -oocmnf 8881   RR*cxr 8882
This theorem is referenced by:  mnfxr  10472  elxr  10474  pnfnemnf  10475  xrltnr  10478  ltpnf  10479  mnfltpnf  10481  pnfnlt  10483  pnfge  10485  nltpnft  10511  xrre  10514  xrre2  10515  xnegex  10551  xnegcl  10556  xaddval  10566  xaddf  10567  xmulval  10568  xaddpnf1  10569  xaddpnf2  10570  pnfaddmnf  10573  mnfaddpnf  10574  xaddass2  10586  xlt2add  10596  xsubge0  10597  xmulneg1  10605  xmulf  10608  xmulpnf1  10610  xmulpnf2  10611  xmulmnf1  10612  xmulpnf1n  10614  xlemul1a  10624  xadddilem  10630  xadddi2  10633  xrsupsslem  10641  xrinfmsslem  10642  xrinfmss  10644  supxrpnf  10653  supxrunb1  10654  supxrunb2  10655  supxrbnd  10663  xrinfm0  10671  elioc2  10729  elico2  10730  elicc2  10731  ioomax  10740  iccmax  10741  ioopos  10742  elioopnf  10753  elicopnf  10755  unirnioo  10759  elxrge0  10763  difreicc  10783  ioopnfsup  10984  icopnfsup  10985  xrsup  10988  hashgval  11356  hashinf  11358  hashbnd  11359  hashf  11360  hashxrcl  11367  hashdomi  11378  rexico  11853  limsupgre  11971  rlim3  11988  pcval  12913  pc0  12923  pcxcl  12929  pc2dvds  12947  pcadd  12953  ramcl2  13079  ramxrcl  13080  ramubcl  13081  abvf  15604  xrsdsreclblem  16433  rege0subm  16444  leordtvallem1  16956  leordtval2  16958  lecldbas  16965  pnfnei  16966  mnfnei  16967  xblpnf  17969  blssec  17997  blpnfctr  17998  nmoix  18254  icopnfcld  18293  iocmnfcld  18294  xrtgioo  18328  reconnlem1  18347  xrge0tsms  18355  metdstri  18371  iccpnfcnv  18458  iccpnfhmeo  18459  cphsqrcl  18636  ovolf  18857  ovollb2lem  18863  ovollb2  18864  ovolunlem1a  18871  ovolunlem1  18872  ovoliunlem1  18877  ovolicc1  18891  ovolicc2lem4  18895  ovolicopnf  18899  ovolre  18900  volsup  18929  ioombl1lem2  18932  ioombl1lem4  18934  icombl1  18936  icombl  18937  ioombl  18938  uniioombllem1  18952  uniioombllem2  18954  uniioombllem3  18956  uniioombllem6  18959  mbfdm  18999  ismbfd  19011  mbfmax  19020  ismbf3d  19025  0plef  19043  mbfi1fseqlem3  19088  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  itg2ge0  19106  itg2mulclem  19117  itg2mulc  19118  itg2monolem1  19121  itg2mono  19124  itg2i1fseq  19126  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  lhop2  19378  dvfsumlem2  19390  dvfsumrlim  19394  dvfsumrlim2  19395  taylfvallem1  19752  taylfval  19754  tayl0  19757  radcnvcl  19809  radcnvle  19812  psercnlem1  19817  logccv  20026  cxpcn3  20104  rlimcnp  20276  rlimcnp2  20277  rlimcnp3  20278  xrlimcnp  20279  efrlim  20280  jensenlem1  20297  jensenlem2  20298  amgm  20301  logfacbnd3  20478  chebbnd1  20637  chebbnd2  20642  dchrisumlem3  20656  log2sumbnd  20709  pntpbnd1  20751  pntibndlem2  20756  pntlemb  20762  pntleme  20773  pnt  20779  isblo3i  21395  xgtpnf  23130  elxrge02  23132  xdivpnfrp  23133  xrdifh  23288  unitssxrge0  23299  tpr2rico  23311  xrge0iifcnv  23330  xrge0iifcv  23331  xrge0iifiso  23332  xrge0iifhom  23334  xrge0mulc1cn  23338  xrge0addass  23344  xrge0neqmnf  23345  xrge0addgt0  23346  xrge0adddir  23347  xrge0npcan  23348  fsumrp0cl  23349  lmlimxrge0  23387  rge0scvg  23388  pnfneige0  23389  lmxrge0  23390  lmdvg  23391  xrge0tsmsd  23397  esum0  23443  esumle  23448  esumlef  23450  esumcst  23451  esumpr2  23454  esumpinfval  23456  esumpfinvallem  23457  esumpfinval  23458  esumpfinvalf  23459  esumpinfsum  23460  esumpcvgval  23461  esummulc1  23464  hashf2  23467  esumcvg  23469  probmeasb  23648  orvcgteel  23683  dstfrvclim1  23693  umgrafi  23889  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  areacirclem4  25030  truni1  25608  oibbi1  25612  dvconstbi  27654  rfcnpre3  27807  sgnpnf  28504
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-pow 4204  ax-un 4528  ax-cnex 8809
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-v 2803  df-un 3170  df-in 3172  df-ss 3179  df-pw 3640  df-sn 3659  df-pr 3660  df-uni 3844  df-pnf 8885  df-xr 8887
  Copyright terms: Public domain W3C validator