Theorem mnfxr 8326

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

Step	Hyp	Ref	Expression
1		df-mnf 8307	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 8323	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4295	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2305	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 3797	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3386	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 8308	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2308	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2203  Vcvv 2812   ∪ cun 3208  𝒫 cpw 3668  {cpr 3689  ℝcr 8122  +∞cpnf 8301  -∞cmnf 8302  ℝ^*cxr 8303

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-un 4553  ax-cnex 8214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-uni 3914  df-pnf 8306  df-mnf 8307  df-xr 8308

This theorem is referenced by:  elxr  10105  xrltnr  10108  mnflt  10112  mnfltpnf  10114  nltmnf  10117  mnfle  10121  xrltnsym  10122  xrlttri3  10126  ngtmnft  10146  xrrebnd  10148  xrre2  10150  xrre3  10151  ge0gtmnf  10152  xnegcl  10161  xltnegi  10164  xaddf  10173  xaddval  10174  xaddmnf1  10177  xaddmnf2  10178  pnfaddmnf  10179  mnfaddpnf  10180  xrex  10185  xltadd1  10205  xlt2add  10209  xsubge0  10210  xposdif  10211  xleaddadd  10216  elioc2  10265  elico2  10266  elicc2  10267  ioomax  10277  iccmax  10278  elioomnf  10297  unirnioo  10302  xrmaxadd  11939  reopnap  15398  blssioo  15405  tgioo  15406  repiecelem  16796  repiecele0  16797  repiecege0  16798