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

Proof

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