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