# Metamath Proof Explorer

## Theorem iccssioo2

Description: Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015)

Ref Expression
Assertion iccssioo2 ${⊢}\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 ne0i ${⊢}{C}\in \left({A},{B}\right)\to \left({A},{B}\right)\ne \varnothing$
2 1 adantr ${⊢}\left({C}\in \left({A},{B}\right)\wedge {D}\in \left({A},{B}\right)\right)\to \left({A},{B}\right)\ne \varnothing$
3 ndmioo ${⊢}¬\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A},{B}\right)=\varnothing$
4 3 necon1ai ${⊢}\left({A},{B}\right)\ne \varnothing \to \left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)$
5 2 4 syl ${⊢}\left({C}\in \left({A},{B}\right)\wedge {D}\in \left({A},{B}\right)\right)\to \left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)$
6 eliooord ${⊢}{C}\in \left({A},{B}\right)\to \left({A}<{C}\wedge {C}<{B}\right)$
7 6 adantr ${⊢}\left({C}\in \left({A},{B}\right)\wedge {D}\in \left({A},{B}\right)\right)\to \left({A}<{C}\wedge {C}<{B}\right)$
8 7 simpld ${⊢}\left({C}\in \left({A},{B}\right)\wedge {D}\in \left({A},{B}\right)\right)\to {A}<{C}$
9 eliooord ${⊢}{D}\in \left({A},{B}\right)\to \left({A}<{D}\wedge {D}<{B}\right)$
10 9 adantl ${⊢}\left({C}\in \left({A},{B}\right)\wedge {D}\in \left({A},{B}\right)\right)\to \left({A}<{D}\wedge {D}<{B}\right)$
11 10 simprd ${⊢}\left({C}\in \left({A},{B}\right)\wedge {D}\in \left({A},{B}\right)\right)\to {D}<{B}$
12 iccssioo ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}<{C}\wedge {D}<{B}\right)\right)\to \left[{C},{D}\right]\subseteq \left({A},{B}\right)$
13 5 8 11 12 syl12anc ${⊢}\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)$