Metamath Proof Explorer

Theorem iccssxr

Description: A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008) (Revised by Mario Carneiro, 4-Jul-2014)

Ref Expression
Assertion iccssxr ( 𝐴 [,] 𝐵 ) ⊆ ℝ*

Proof

Step Hyp Ref Expression
1 df-icc ⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
2 1 ixxssxr ⊢ ( 𝐴 [,] 𝐵 ) ⊆ ℝ*