ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mnfxr GIF version

Theorem mnfxr 8012
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 -∞ ∈ ℝ*

Proof of Theorem mnfxr
StepHypRef Expression
1 df-mnf 7993 . . . . 5 -∞ = 𝒫 +∞
2 pnfex 8009 . . . . . 6 +∞ ∈ V
32pwex 4183 . . . . 5 𝒫 +∞ ∈ V
41, 3eqeltri 2250 . . . 4 -∞ ∈ V
54prid2 3699 . . 3 -∞ ∈ {+∞, -∞}
6 elun2 3303 . . 3 (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
75, 6ax-mp 5 . 2 -∞ ∈ (ℝ ∪ {+∞, -∞})
8 df-xr 7994 . 2 * = (ℝ ∪ {+∞, -∞})
97, 8eleqtrri 2253 1 -∞ ∈ ℝ*
Colors of variables: wff set class
Syntax hints:  wcel 2148  Vcvv 2737  cun 3127  𝒫 cpw 3575  {cpr 3593  cr 7809  +∞cpnf 7987  -∞cmnf 7988  *cxr 7989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-un 4433  ax-cnex 7901
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-uni 3810  df-pnf 7992  df-mnf 7993  df-xr 7994
This theorem is referenced by:  elxr  9774  xrltnr  9777  mnflt  9781  mnfltpnf  9783  nltmnf  9786  mnfle  9790  xrltnsym  9791  xrlttri3  9795  ngtmnft  9815  xrrebnd  9817  xrre2  9819  xrre3  9820  ge0gtmnf  9821  xnegcl  9830  xltnegi  9833  xaddf  9842  xaddval  9843  xaddmnf1  9846  xaddmnf2  9847  pnfaddmnf  9848  mnfaddpnf  9849  xrex  9854  xltadd1  9874  xlt2add  9878  xsubge0  9879  xposdif  9880  xleaddadd  9885  elioc2  9934  elico2  9935  elicc2  9936  ioomax  9946  iccmax  9947  elioomnf  9966  unirnioo  9971  xrmaxadd  11264  reopnap  13931  blssioo  13938  tgioo  13939
  Copyright terms: Public domain W3C validator