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

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

Proof

Step Hyp Ref Expression
1 df-icc ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x ≤ z ∧ z ≤ y
2 1 elixx3g ⊢ C ∈ A B ↔ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A ≤ C ∧ C ≤ B
3 2 simplbi ⊢ C ∈ A B → A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ *
4 3 adantr ⊢ C ∈ A B ∧ D ∈ A B → A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ *
5 4 simp1d ⊢ C ∈ A B ∧ D ∈ A B → A ∈ ℝ *
6 4 simp2d ⊢ C ∈ A B ∧ D ∈ A B → B ∈ ℝ *
7 2 simprbi ⊢ C ∈ A B → A ≤ C ∧ C ≤ B
8 7 adantr ⊢ C ∈ A B ∧ D ∈ A B → A ≤ C ∧ C ≤ B
9 8 simpld ⊢ C ∈ A B ∧ D ∈ A B → A ≤ C
10 1 elixx3g ⊢ D ∈ A B ↔ A ∈ ℝ * ∧ B ∈ ℝ * ∧ D ∈ ℝ * ∧ A ≤ D ∧ D ≤ B
11 10 simprbi ⊢ D ∈ A B → A ≤ D ∧ D ≤ B
12 11 simprd ⊢ D ∈ A B → D ≤ B
13 12 adantl ⊢ C ∈ A B ∧ D ∈ A B → D ≤ B
14 xrletr ⊢ A ∈ ℝ * ∧ C ∈ ℝ * ∧ w ∈ ℝ * → A ≤ C ∧ C ≤ w → A ≤ w
15 xrletr ⊢ w ∈ ℝ * ∧ D ∈ ℝ * ∧ B ∈ ℝ * → w ≤ D ∧ D ≤ B → w ≤ B
16 1 1 14 15 ixxss12 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ C ∧ D ≤ B → C D ⊆ A B
17 5 6 9 13 16 syl22anc ⊢ C ∈ A B ∧ D ∈ A B → C D ⊆ A B