iccmax

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

		Ref	Expression
	Assertion	iccmax	$⊢ [−∞, +∞] = ℝ^{*}$

Step	Hyp	Ref	Expression
1		mnfxr	$⊢ −∞ \in ℝ^{*}$
2		pnfxr	$⊢ +∞ \in ℝ^{*}$
3		iccval	$⊢ (−∞ \in ℝ^{} \land +∞ \in ℝ^{}) \to [−∞, +∞] = \{x \in ℝ^{*} \| (−∞ \leq x \land x \leq +∞)\}$
4	1 2 3	mp2an	$⊢ [−∞, +∞] = \{x \in ℝ^{*} \| (−∞ \leq x \land x \leq +∞)\}$
5		rabid2	$⊢ ℝ^{} = \{x \in ℝ^{} \| (−∞ \leq x \land x \leq +∞)\} \leftrightarrow \forall x \in ℝ^{*} (−∞ \leq x \land x \leq +∞)$
6		mnfle	$⊢ x \in ℝ^{*} \to −∞ \leq x$
7		pnfge	$⊢ x \in ℝ^{*} \to x \leq +∞$
8	6 7	jca	$⊢ x \in ℝ^{*} \to (−∞ \leq x \land x \leq +∞)$
9	5 8	mprgbir	$⊢ ℝ^{} = \{x \in ℝ^{} \| (−∞ \leq x \land x \leq +∞)\}$
10	4 9	eqtr4i	$⊢ [−∞, +∞] = ℝ^{*}$

Metamath Proof Explorer