Metamath Proof Explorer


Theorem iocssicc

Description: A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017)

Ref Expression
Assertion iocssicc ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )

Proof

Step Hyp Ref Expression
1 df-ioc (,] = ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑥 ∈ ℝ* ∣ ( 𝑎 < 𝑥𝑥𝑏 ) } )
2 df-icc [,] = ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑥 ∈ ℝ* ∣ ( 𝑎𝑥𝑥𝑏 ) } )
3 xrltle ( ( 𝐴 ∈ ℝ*𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤𝐴𝑤 ) )
4 idd ( ( 𝑤 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝑤𝐵𝑤𝐵 ) )
5 1 2 3 4 ixxssixx ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )