Theorem mnfxr

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)

	Ref	Expression
Assertion	mnfxr	⊢ -∞ ∈ ℝ*

Proof

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