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 ( -∞ [,] +∞ ) = ℝ*

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 ( -∞ [,] +∞ ) = ℝ*