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\}\leftrightarrow \forall x\in {ℝ}^{*}\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]={ℝ}^{*}$$