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

Theorem mnfxr 8076
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 8057 . . . . 5 -∞ = 𝒫 +∞
2 pnfex 8073 . . . . . 6 +∞ ∈ V
32pwex 4212 . . . . 5 𝒫 +∞ ∈ V
41, 3eqeltri 2266 . . . 4 -∞ ∈ V
54prid2 3725 . . 3 -∞ ∈ {+∞, -∞}
6 elun2 3327 . . 3 (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
75, 6ax-mp 5 . 2 -∞ ∈ (ℝ ∪ {+∞, -∞})
8 df-xr 8058 . 2 * = (ℝ ∪ {+∞, -∞})
97, 8eleqtrri 2269 1 -∞ ∈ ℝ*
Colors of variables: wff set class
Syntax hints:  wcel 2164  Vcvv 2760  cun 3151  𝒫 cpw 3601  {cpr 3619  cr 7871  +∞cpnf 8051  -∞cmnf 8052  *cxr 8053
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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-un 4464  ax-cnex 7963
This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-uni 3836  df-pnf 8056  df-mnf 8057  df-xr 8058
This theorem is referenced by:  elxr  9842  xrltnr  9845  mnflt  9849  mnfltpnf  9851  nltmnf  9854  mnfle  9858  xrltnsym  9859  xrlttri3  9863  ngtmnft  9883  xrrebnd  9885  xrre2  9887  xrre3  9888  ge0gtmnf  9889  xnegcl  9898  xltnegi  9901  xaddf  9910  xaddval  9911  xaddmnf1  9914  xaddmnf2  9915  pnfaddmnf  9916  mnfaddpnf  9917  xrex  9922  xltadd1  9942  xlt2add  9946  xsubge0  9947  xposdif  9948  xleaddadd  9953  elioc2  10002  elico2  10003  elicc2  10004  ioomax  10014  iccmax  10015  elioomnf  10034  unirnioo  10039  xrmaxadd  11404  reopnap  14706  blssioo  14713  tgioo  14714
  Copyright terms: Public domain W3C validator