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	⊢ ( ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 [,] 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ne0i	⊢ ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
2	1	adantr	⊢ ( ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
3		ndmioo	⊢ ( ¬ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) = ∅ )
4	3	necon1ai	⊢ ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
5	2 4	syl	⊢ ( ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
6		eliooord	⊢ ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) )
7	6	adantr	⊢ ( ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) )
8	7	simpld	⊢ ( ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝐶 )
9		eliooord	⊢ ( 𝐷 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝐷 ∧ 𝐷 < 𝐵 ) )
10	9	adantl	⊢ ( ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 < 𝐷 ∧ 𝐷 < 𝐵 ) )
11	10	simprd	⊢ ( ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐷 < 𝐵 )
12		iccssioo	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐶 ∧ 𝐷 < 𝐵 ) ) → ( 𝐶 [,] 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
13	5 8 11 12	syl12anc	⊢ ( ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 [,] 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )