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

Theorem mnfxr 7929
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 7910 . . . . 5 -∞ = 𝒫 +∞
2 pnfex 7926 . . . . . 6 +∞ ∈ V
32pwex 4144 . . . . 5 𝒫 +∞ ∈ V
41, 3eqeltri 2230 . . . 4 -∞ ∈ V
54prid2 3666 . . 3 -∞ ∈ {+∞, -∞}
6 elun2 3275 . . 3 (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
75, 6ax-mp 5 . 2 -∞ ∈ (ℝ ∪ {+∞, -∞})
8 df-xr 7911 . 2 * = (ℝ ∪ {+∞, -∞})
97, 8eleqtrri 2233 1 -∞ ∈ ℝ*
Colors of variables: wff set class
Syntax hints:  wcel 2128  Vcvv 2712  cun 3100  𝒫 cpw 3543  {cpr 3561  cr 7726  +∞cpnf 7904  -∞cmnf 7905  *cxr 7906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-un 4393  ax-cnex 7818
This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-uni 3773  df-pnf 7909  df-mnf 7910  df-xr 7911
This theorem is referenced by:  elxr  9678  xrltnr  9681  mnflt  9685  mnfltpnf  9687  nltmnf  9690  mnfle  9694  xrltnsym  9695  xrlttri3  9699  ngtmnft  9716  xrrebnd  9718  xrre2  9720  xrre3  9721  ge0gtmnf  9722  xnegcl  9731  xltnegi  9734  xaddf  9743  xaddval  9744  xaddmnf1  9747  xaddmnf2  9748  pnfaddmnf  9749  mnfaddpnf  9750  xrex  9755  xltadd1  9775  xlt2add  9779  xsubge0  9780  xposdif  9781  xleaddadd  9786  elioc2  9835  elico2  9836  elicc2  9837  ioomax  9847  iccmax  9848  elioomnf  9867  unirnioo  9872  xrmaxadd  11153  reopnap  12925  blssioo  12932  tgioo  12933
  Copyright terms: Public domain W3C validator