# Metamath Proof Explorer

## Theorem icossico

Description: Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Thierry Arnoux, 21-Sep-2017)

Ref Expression
Assertion icossico ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}\le {C}\wedge {D}\le {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 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)$
3 xrltletr ${⊢}\left({w}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({w}<{D}\wedge {D}\le {B}\right)\to {w}<{B}\right)$
4 1 1 2 3 ixxss12 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}\le {C}\wedge {D}\le {B}\right)\right)\to \left[{C},{D}\right)\subseteq \left[{A},{B}\right)$