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

Theorem mnfxr 10472
Description: Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
Assertion
Ref Expression
mnfxr  |-  -oo  e.  RR*

Proof of Theorem mnfxr
StepHypRef Expression
1 df-mnf 8886 . . . . 5  |-  -oo  =  ~P  +oo
2 pnfxr 10471 . . . . . . 7  |-  +oo  e.  RR*
32elexi 2810 . . . . . 6  |-  +oo  e.  _V
43pwex 4209 . . . . 5  |-  ~P  +oo  e.  _V
51, 4eqeltri 2366 . . . 4  |-  -oo  e.  _V
65prid2 3748 . . 3  |-  -oo  e.  { 
+oo ,  -oo }
7 elun2 3356 . . 3  |-  (  -oo  e.  {  +oo ,  -oo }  ->  -oo  e.  ( RR  u.  {  +oo ,  -oo } ) )
86, 7ax-mp 8 . 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   RRcr 8752    +oocpnf 8880    -oocmnf 8881   RR*cxr 8882
This theorem is referenced by:  elxr  10474  xrltnr  10478  mnflt  10480  mnfltpnf  10481  nltmnf  10484  mnfle  10486  xrltnsym  10487  ngtmnft  10512  xrre2  10515  xrre3  10516  ge0gtmnf  10517  xnegex  10551  xnegcl  10556  xltnegi  10559  xaddval  10566  xaddf  10567  xmulval  10568  xaddmnf1  10571  xaddmnf2  10572  pnfaddmnf  10573  mnfaddpnf  10574  xlt2add  10596  xsubge0  10597  xmulneg1  10605  xmulf  10608  xmulmnf2  10613  xmulpnf1n  10614  xadddilem  10630  xadddi2  10633  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  supxrmnf  10652  xrsup0  10658  supxrre  10662  infmxrre  10670  elioc2  10729  elico2  10730  elicc2  10731  ioomax  10740  iccmax  10741  elioomnf  10754  unirnioo  10759  difreicc  10783  resup  10987  caucvgrlem  12161  xrsdsreclblem  16433  leordtvallem2  16957  leordtval2  16958  lecldbas  16965  pnfnei  16966  mnfnei  16967  icopnfcld  18293  iocmnfcld  18294  blssioo  18317  tgioo  18318  xrtgioo  18328  reconnlem1  18347  reconnlem2  18348  bndth  18472  ovolunnul  18875  ovoliunlem1  18877  ovoliun  18880  ovolicopnf  18899  voliunlem3  18925  volsup  18929  ioombl1lem2  18932  ioombl  18938  volivth  18978  mbfdm  18999  ismbfd  19011  mbfmax  19020  ismbf3d  19025  itg2seq  19113  itg2monolem2  19122  dvferm1lem  19347  dvferm2lem  19349  mdegcl  19471  plypf1  19610  ellogdm  20002  logdmnrp  20004  dvloglem  20011  dvlog2lem  20015  atans2  20243  ressatans  20246  xrre3FL  23266  supxrnemnf  23271  xrdifh  23288  tpr2rico  23311  xrge00  23326  xrge0iifcnv  23330  xrge0neqmnf  23345  xrge0adddir  23347  fsumrp0cl  23349  lmlimxrge0  23387  rge0scvg  23388  lmdvg  23391  esumpfinvallem  23457  esumpfinval  23458  esumpfinvalf  23459  esumpcvgval  23461  esumcvg  23469  dya2iocbrsiga  23593  orvclteel  23688  itg2gt0cn  25006  dvreasin  25026  areacirclem5  25032  areacirclem6  25033  oibbi2  25613  rfcnpre4  27808  sgnmnf  28506
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-mnf 8886  df-xr 8887
  Copyright terms: Public domain W3C validator