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 \in [A, B] \land D \in [A, B]) \to [C, D] \subseteq [A, B]$

Proof

Step	Hyp	Ref	Expression
1		df-icc	$⊢ [.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\})$
2	1	elixx3g	$⊢ C \in [A, B] \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq C \land C \leq B))$
3	2	simplbi	$⊢ C \in [A, B] \to (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*})$
4	3	adantr	$⊢ (C \in [A, B] \land D \in [A, B]) \to (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*})$
5	4	simp1d	$⊢ (C \in [A, B] \land D \in [A, B]) \to A \in ℝ^{*}$
6	4	simp2d	$⊢ (C \in [A, B] \land D \in [A, B]) \to B \in ℝ^{*}$
7	2	simprbi	$⊢ C \in [A, B] \to (A \leq C \land C \leq B)$
8	7	adantr	$⊢ (C \in [A, B] \land D \in [A, B]) \to (A \leq C \land C \leq B)$
9	8	simpld	$⊢ (C \in [A, B] \land D \in [A, B]) \to A \leq C$
10	1	elixx3g	$⊢ D \in [A, B] \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land D \in ℝ^{*}) \land (A \leq D \land D \leq B))$
11	10	simprbi	$⊢ D \in [A, B] \to (A \leq D \land D \leq B)$
12	11	simprd	$⊢ D \in [A, B] \to D \leq B$
13	12	adantl	$⊢ (C \in [A, B] \land D \in [A, B]) \to D \leq B$
14		xrletr	$⊢ (A \in ℝ^{} \land C \in ℝ^{} \land w \in ℝ^{*}) \to ((A \leq C \land C \leq w) \to A \leq w)$
15		xrletr	$⊢ (w \in ℝ^{} \land D \in ℝ^{} \land B \in ℝ^{*}) \to ((w \leq D \land D \leq B) \to w \leq B)$
16	1 1 14 15	ixxss12	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A \leq C \land D \leq B)) \to [C, D] \subseteq [A, B]$
17	5 6 9 13 16	syl22anc	$⊢ (C \in [A, B] \land D \in [A, B]) \to [C, D] \subseteq [A, B]$