This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ -∞ ∈ ℝ^*