# Metamath Proof Explorer

## Theorem iccssico

Description: Condition for a closed interval to be a subset of a half-open interval. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion iccssico ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}\le {C}\wedge {D}<{B}\right)\right)\to \left[{C},{D}\right]\subseteq \left[{A},{B}\right)$

### Proof

Step Hyp Ref Expression
1 df-ico ${⊢}\left[.\right)=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)$
2 df-icc ${⊢}\left[.\right]=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}\le {y}\right)\right\}\right)$
3 xrletr ${⊢}\left({A}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(\left({A}\le {C}\wedge {C}\le {w}\right)\to {A}\le {w}\right)$
4 xrlelttr ${⊢}\left({w}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({w}\le {D}\wedge {D}<{B}\right)\to {w}<{B}\right)$
5 1 2 3 4 ixxss12 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}\le {C}\wedge {D}<{B}\right)\right)\to \left[{C},{D}\right]\subseteq \left[{A},{B}\right)$