Metamath Proof Explorer


Theorem ioossioc

Description: An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion ioossioc ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,] 𝐵 )

Proof

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