Theorem iccmax

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

	Ref	Expression
Assertion	iccmax	⊢ ( -∞ [,] +∞ ) = ℝ*

Proof

Step	Hyp	Ref	Expression
1		mnfxr	⊢ -∞ ∈ ℝ*
2		pnfxr	⊢ +∞ ∈ ℝ*
3		iccval	⊢ ( ( -∞ ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( -∞ [,] +∞ ) = { 𝑥 ∈ ℝ* ∣ ( -∞ ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) } )
4	1 2 3	mp2an	⊢ ( -∞ [,] +∞ ) = { 𝑥 ∈ ℝ* ∣ ( -∞ ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) }
5		rabid2	⊢ ( ℝ* = { 𝑥 ∈ ℝ* ∣ ( -∞ ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) } ↔ ∀ 𝑥 ∈ ℝ* ( -∞ ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) )
6		mnfle	⊢ ( 𝑥 ∈ ℝ* → -∞ ≤ 𝑥 )
7		pnfge	⊢ ( 𝑥 ∈ ℝ* → 𝑥 ≤ +∞ )
8	6 7	jca	⊢ ( 𝑥 ∈ ℝ* → ( -∞ ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) )
9	5 8	mprgbir	⊢ ℝ* = { 𝑥 ∈ ℝ* ∣ ( -∞ ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) }
10	4 9	eqtr4i	⊢ ( -∞ [,] +∞ ) = ℝ*