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 | |- -oo e. RR* |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-mnf | |- -oo = ~P +oo |
|
| 2 | pnfex | |- +oo e. _V |
|
| 3 | 2 | pwex | |- ~P +oo e. _V |
| 4 | 1 3 | eqeltri | |- -oo e. _V |
| 5 | 4 | prid2 | |- -oo e. { +oo , -oo } |
| 6 | elun2 | |- ( -oo e. { +oo , -oo } -> -oo e. ( RR u. { +oo , -oo } ) ) |
|
| 7 | 5 6 | ax-mp | |- -oo e. ( RR u. { +oo , -oo } ) |
| 8 | df-xr | |- RR* = ( RR u. { +oo , -oo } ) |
|
| 9 | 7 8 | eleqtrri | |- -oo e. RR* |