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

Metamath Proof Explorer

Theorem icossico

Description: Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Thierry Arnoux, 21-Sep-2017)

		Ref	Expression
	Assertion	icossico	$⊢ ((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		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
2		xrletr	$⊢ (A \in ℝ^{} \land C \in ℝ^{} \land w \in ℝ^{*}) \to ((A \leq C \land C \leq w) \to A \leq w)$
3		xrltletr	$⊢ (w \in ℝ^{} \land D \in ℝ^{} \land B \in ℝ^{*}) \to ((w < D \land D \leq B) \to w < B)$
4	1 1 2 3	ixxss12	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A \leq C \land D \leq B)) \to [C, D) \subseteq [A, B)$