Description: An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | ioossioc | ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,] 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ioo | ⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } ) | |
2 | df-ioc | ⊢ (,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ) | |
3 | idd | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤 → 𝐴 < 𝑤 ) ) | |
4 | xrltle | ⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑤 < 𝐵 → 𝑤 ≤ 𝐵 ) ) | |
5 | 1 2 3 4 | ixxssixx | ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,] 𝐵 ) |