This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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