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 ⊢ C ∈ A B ∧ D ∈ A B → C D ⊆ A B

Proof

Step Hyp Ref Expression
1 ne0i ⊢ C ∈ A B → A B ≠ ∅
2 1 adantr ⊢ C ∈ A B ∧ D ∈ A B → A B ≠ ∅
3 ndmioo ⊢ ¬ A ∈ ℝ * ∧ B ∈ ℝ * → A B = ∅
4 3 necon1ai ⊢ A B ≠ ∅ → A ∈ ℝ * ∧ B ∈ ℝ *
5 2 4 syl ⊢ C ∈ A B ∧ D ∈ A B → A ∈ ℝ * ∧ B ∈ ℝ *
6 eliooord ⊢ C ∈ A B → A < C ∧ C < B
7 6 adantr ⊢ C ∈ A B ∧ D ∈ A B → A < C ∧ C < B
8 7 simpld ⊢ C ∈ A B ∧ D ∈ A B → A < C
9 eliooord ⊢ D ∈ A B → A < D ∧ D < B
10 9 adantl ⊢ C ∈ A B ∧ D ∈ A B → A < D ∧ D < B
11 10 simprd ⊢ C ∈ A B ∧ D ∈ A B → D < B
12 iccssioo ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A < C ∧ D < B → C D ⊆ A B
13 5 8 11 12 syl12anc ⊢ C ∈ A B ∧ D ∈ A B → C D ⊆ A B