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	$⊢ −∞ \in ℝ^{*}$

Proof

Step	Hyp	Ref	Expression
1		df-mnf	$⊢ −∞ = 𝒫 +∞$
2		pnfex	$⊢ +∞ \in V$
3	2	pwex	$⊢ 𝒫 +∞ \in V$
4	1 3	eqeltri	$⊢ −∞ \in V$
5	4	prid2	$⊢ −∞ \in \{+∞, −∞\}$
6		elun2	$⊢ −∞ \in \{+∞, −∞\} \to −∞ \in (ℝ \cup \{+∞, −∞\})$
7	5 6	ax-mp	$⊢ −∞ \in (ℝ \cup \{+∞, −∞\})$
8		df-xr	$⊢ ℝ^{*} = ℝ \cup \{+∞, −∞\}$
9	7 8	eleqtrri	$⊢ −∞ \in ℝ^{*}$