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

Theorem mnfxr 11197
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 9524 . . . . 5  |- -oo  =  ~P +oo
2 pnfex 11196 . . . . . 6  |- +oo  e.  _V
32pwex 4575 . . . . 5  |-  ~P +oo  e.  _V
41, 3eqeltri 2535 . . . 4  |- -oo  e.  _V
54prid2 4084 . . 3  |- -oo  e.  { +oo , -oo }
6 elun2 3624 . . 3  |-  ( -oo  e.  { +oo , -oo }  -> -oo  e.  ( RR  u.  { +oo , -oo } ) )
75, 6ax-mp 5 . 2  |- -oo  e.  ( RR  u.  { +oo , -oo } )
8 df-xr 9525 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
97, 8eleqtrri 2538 1  |- -oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   _Vcvv 3070    u. cun 3426   ~Pcpw 3960   {cpr 3979   RRcr 9384   +oocpnf 9518   -oocmnf 9519   RR*cxr 9520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4513  ax-pow 4570  ax-un 6474  ax-cnex 9441
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rex 2801  df-v 3072  df-un 3433  df-in 3435  df-ss 3442  df-pw 3962  df-sn 3978  df-pr 3980  df-uni 4192  df-pnf 9523  df-mnf 9524  df-xr 9525
This theorem is referenced by:  elxr  11199  xrltnr  11204  mnflt  11207  mnfltpnf  11209  nltmnf  11212  mnfle  11216  xrltnsym  11217  ngtmnft  11242  xrre2  11245  xrre3  11246  ge0gtmnf  11247  xnegex  11281  xnegcl  11286  xltnegi  11289  xaddval  11296  xaddf  11297  xmulval  11298  xaddmnf1  11301  xaddmnf2  11302  pnfaddmnf  11303  mnfaddpnf  11304  xlt2add  11326  xsubge0  11327  xmulneg1  11335  xmulf  11338  xmulmnf2  11343  xmulpnf1n  11344  xadddilem  11360  xadddi2  11363  xrsupsslem  11372  xrinfmsslem  11373  xrub  11377  supxrmnf  11383  xrsup0  11389  supxrre  11393  infmxrre  11401  elioc2  11461  elico2  11462  elicc2  11463  ioomax  11473  iccmax  11474  elioomnf  11487  unirnioo  11492  difreicc  11520  resup  11809  sgnmnf  12688  caucvgrlem  13254  xrsdsreclblem  17970  leordtvallem2  18933  leordtval2  18934  lecldbas  18941  pnfnei  18942  mnfnei  18943  icopnfcld  20465  iocmnfcld  20466  blssioo  20490  tgioo  20491  xrtgioo  20501  reconnlem1  20521  reconnlem2  20522  bndth  20648  ovolunnul  21101  ovoliunlem1  21103  ovoliun  21106  ovolicopnf  21125  voliunlem3  21151  volsup  21155  ioombl1lem2  21158  ioombl  21164  volivth  21205  mbfdm  21224  ismbfd  21236  mbfmax  21245  ismbf3d  21250  itg2seq  21338  itg2monolem2  21347  dvferm1lem  21574  dvferm2lem  21576  mdegcl  21658  plypf1  21798  ellogdm  22202  logdmnrp  22204  dvloglem  22211  dvlog2lem  22215  atans2  22444  ressatans  22447  xlemnf  26180  xrinfm  26184  supxrnemnf  26192  xrdifh  26206  xrge00  26283  xrge0neqmnf  26288  tpr2rico  26478  xrge0iifcnv  26499  esumfsupre  26656  esumpfinvallem  26659  esumpcvgval  26663  esumcvg  26671  dya2iocbrsiga  26826  dya2icobrsiga  26827  orvclteel  26991  itg2gt0cn  28587  asindmre  28619  dvasin  28620  dvacos  28621  areacirclem4  28627  areacirclem5  28628  rfcnpre4  29896
  Copyright terms: Public domain W3C validator