# Metamath Proof Explorer

## Theorem iccmax

Description: The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014)

Ref Expression
Assertion iccmax ${⊢}\left[\mathrm{-\infty },\mathrm{+\infty }\right]={ℝ}^{*}$

### Proof

Step Hyp Ref Expression
1 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
2 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
3 iccval ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left[\mathrm{-\infty },\mathrm{+\infty }\right]=\left\{{x}\in {ℝ}^{*}|\left(\mathrm{-\infty }\le {x}\wedge {x}\le \mathrm{+\infty }\right)\right\}$
4 1 2 3 mp2an ${⊢}\left[\mathrm{-\infty },\mathrm{+\infty }\right]=\left\{{x}\in {ℝ}^{*}|\left(\mathrm{-\infty }\le {x}\wedge {x}\le \mathrm{+\infty }\right)\right\}$
5 rabid2 ${⊢}{ℝ}^{*}=\left\{{x}\in {ℝ}^{*}|\left(\mathrm{-\infty }\le {x}\wedge {x}\le \mathrm{+\infty }\right)\right\}↔\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\mathrm{-\infty }\le {x}\wedge {x}\le \mathrm{+\infty }\right)$
6 mnfle ${⊢}{x}\in {ℝ}^{*}\to \mathrm{-\infty }\le {x}$
7 pnfge ${⊢}{x}\in {ℝ}^{*}\to {x}\le \mathrm{+\infty }$
8 6 7 jca ${⊢}{x}\in {ℝ}^{*}\to \left(\mathrm{-\infty }\le {x}\wedge {x}\le \mathrm{+\infty }\right)$
9 5 8 mprgbir ${⊢}{ℝ}^{*}=\left\{{x}\in {ℝ}^{*}|\left(\mathrm{-\infty }\le {x}\wedge {x}\le \mathrm{+\infty }\right)\right\}$
10 4 9 eqtr4i ${⊢}\left[\mathrm{-\infty },\mathrm{+\infty }\right]={ℝ}^{*}$