Metamath Proof Explorer

Theorem iccss

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, 20-Feb-2015)

		Ref	Expression
	Assertion	iccss	$⊢ ((A \in ℝ \land B \in ℝ) \land (A \leq C \land D \leq B)) \to [C, D] \subseteq [A, B]$

Proof

Step	Hyp	Ref	Expression
1		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
2		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
3	1 2	anim12i	$⊢ (A \in ℝ \land B \in ℝ) \to (A \in ℝ^{} \land B \in ℝ^{})$
4		df-icc	$⊢ [.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\})$
5		xrletr	$⊢ (A \in ℝ^{} \land C \in ℝ^{} \land w \in ℝ^{*}) \to ((A \leq C \land C \leq w) \to A \leq w)$
6		xrletr	$⊢ (w \in ℝ^{} \land D \in ℝ^{} \land B \in ℝ^{*}) \to ((w \leq D \land D \leq B) \to w \leq B)$
7	4 4 5 6	ixxss12	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A \leq C \land D \leq B)) \to [C, D] \subseteq [A, B]$
8	3 7	sylan	$⊢ ((A \in ℝ \land B \in ℝ) \land (A \leq C \land D \leq B)) \to [C, D] \subseteq [A, B]$