icossioo

Description: Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017)

		Ref	Expression
	Assertion	icossioo	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < C \land D \leq B)) \to [C, D) \subseteq (A, B)$

Step	Hyp	Ref	Expression
1		df-ioo	$⊢ (.) = (a \in ℝ^{}, b \in ℝ^{} ⟼ \{x \in ℝ^{*} \| (a < x \land x < b)\})$
2		df-ico	$⊢ [.) = (a \in ℝ^{}, b \in ℝ^{} ⟼ \{x \in ℝ^{*} \| (a \leq x \land x < b)\})$
3		xrltletr	$⊢ (A \in ℝ^{} \land C \in ℝ^{} \land w \in ℝ^{*}) \to ((A < C \land C \leq w) \to A < w)$
4		xrltletr	$⊢ (w \in ℝ^{} \land D \in ℝ^{} \land B \in ℝ^{*}) \to ((w < D \land D \leq B) \to w < B)$
5	1 2 3 4	ixxss12	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < C \land D \leq B)) \to [C, D) \subseteq (A, B)$

Metamath Proof Explorer