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

Theorem mnfxr 8013
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 7994 . . . . 5 -∞ = 𝒫 +∞
2 pnfex 8010 . . . . . 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 7995 . 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 7988  -∞cmnf 7989  *cxr 7990
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 7993  df-mnf 7994  df-xr 7995
This theorem is referenced by:  elxr  9775  xrltnr  9778  mnflt  9782  mnfltpnf  9784  nltmnf  9787  mnfle  9791  xrltnsym  9792  xrlttri3  9796  ngtmnft  9816  xrrebnd  9818  xrre2  9820  xrre3  9821  ge0gtmnf  9822  xnegcl  9831  xltnegi  9834  xaddf  9843  xaddval  9844  xaddmnf1  9847  xaddmnf2  9848  pnfaddmnf  9849  mnfaddpnf  9850  xrex  9855  xltadd1  9875  xlt2add  9879  xsubge0  9880  xposdif  9881  xleaddadd  9886  elioc2  9935  elico2  9936  elicc2  9937  ioomax  9947  iccmax  9948  elioomnf  9967  unirnioo  9972  xrmaxadd  11268  reopnap  14008  blssioo  14015  tgioo  14016
  Copyright terms: Public domain W3C validator