# Metamath Proof Explorer

## Theorem iccss2

Description: Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion iccss2 ${⊢}\left({C}\in \left[{A},{B}\right]\wedge {D}\in \left[{A},{B}\right]\right)\to \left[{C},{D}\right]\subseteq \left[{A},{B}\right]$

### Proof

Step Hyp Ref Expression
1 df-icc ${⊢}\left[.\right]=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}\le {y}\right)\right\}\right)$
2 1 elixx3g ${⊢}{C}\in \left[{A},{B}\right]↔\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}\le {C}\wedge {C}\le {B}\right)\right)$
3 2 simplbi ${⊢}{C}\in \left[{A},{B}\right]\to \left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)$
4 3 adantr ${⊢}\left({C}\in \left[{A},{B}\right]\wedge {D}\in \left[{A},{B}\right]\right)\to \left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)$
5 4 simp1d ${⊢}\left({C}\in \left[{A},{B}\right]\wedge {D}\in \left[{A},{B}\right]\right)\to {A}\in {ℝ}^{*}$
6 4 simp2d ${⊢}\left({C}\in \left[{A},{B}\right]\wedge {D}\in \left[{A},{B}\right]\right)\to {B}\in {ℝ}^{*}$
7 2 simprbi ${⊢}{C}\in \left[{A},{B}\right]\to \left({A}\le {C}\wedge {C}\le {B}\right)$
8 7 adantr ${⊢}\left({C}\in \left[{A},{B}\right]\wedge {D}\in \left[{A},{B}\right]\right)\to \left({A}\le {C}\wedge {C}\le {B}\right)$
9 8 simpld ${⊢}\left({C}\in \left[{A},{B}\right]\wedge {D}\in \left[{A},{B}\right]\right)\to {A}\le {C}$
10 1 elixx3g ${⊢}{D}\in \left[{A},{B}\right]↔\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\right)\wedge \left({A}\le {D}\wedge {D}\le {B}\right)\right)$
11 10 simprbi ${⊢}{D}\in \left[{A},{B}\right]\to \left({A}\le {D}\wedge {D}\le {B}\right)$
12 11 simprd ${⊢}{D}\in \left[{A},{B}\right]\to {D}\le {B}$
13 12 adantl ${⊢}\left({C}\in \left[{A},{B}\right]\wedge {D}\in \left[{A},{B}\right]\right)\to {D}\le {B}$
14 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)$
15 xrletr ${⊢}\left({w}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({w}\le {D}\wedge {D}\le {B}\right)\to {w}\le {B}\right)$
16 1 1 14 15 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]$
17 5 6 9 13 16 syl22anc ${⊢}\left({C}\in \left[{A},{B}\right]\wedge {D}\in \left[{A},{B}\right]\right)\to \left[{C},{D}\right]\subseteq \left[{A},{B}\right]$