iccssico2

Description: Condition for a closed interval to be a subset of a closed-below, open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015)

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

Step	Hyp	Ref	Expression
1		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
2	1	elmpocl1	$⊢ C \in [A, B) \to A \in ℝ^{*}$
3	2	adantr	$⊢ (C \in [A, B) \land D \in [A, B)) \to A \in ℝ^{*}$
4	1	elmpocl2	$⊢ C \in [A, B) \to B \in ℝ^{*}$
5	4	adantr	$⊢ (C \in [A, B) \land D \in [A, B)) \to B \in ℝ^{*}$
6	1	elixx3g	$⊢ C \in [A, B) \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq C \land C < B))$
7	6	simprbi	$⊢ C \in [A, B) \to (A \leq C \land C < B)$
8	7	simpld	$⊢ C \in [A, B) \to A \leq C$
9	8	adantr	$⊢ (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 < B))$
11	10	simprbi	$⊢ D \in [A, B) \to (A \leq D \land D < B)$
12	11	simprd	$⊢ D \in [A, B) \to D < B$
13	12	adantl	$⊢ (C \in [A, B) \land D \in [A, B)) \to D < B$
14		iccssico	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A \leq C \land D < B)) \to [C, D] \subseteq [A, B)$
15	3 5 9 13 14	syl22anc	$⊢ (C \in [A, B) \land D \in [A, B)) \to [C, D] \subseteq [A, B)$

Metamath Proof Explorer