Metamath Proof Explorer

Theorem icoun

Description: The union of two adjacent left-closed right-open real intervals is a left-closed right-open real interval. (Contributed by Paul Chapman, 15-Mar-2008) (Proof shortened by Mario Carneiro, 16-Jun-2014)

		Ref	Expression
	Assertion	icoun	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \to [A, B) \cup [B, C) = [A, C)$

Proof

Step	Hyp	Ref	Expression
1		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
2		xrlenlt	$⊢ (B \in ℝ^{} \land w \in ℝ^{}) \to (B \leq w \leftrightarrow \neg w < B)$
3		xrltletr	$⊢ (w \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((w < B \land B \leq C) \to w < C)$
4		xrletr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land w \in ℝ^{*}) \to ((A \leq B \land B \leq w) \to A \leq w)$
5	1 1 2 1 3 4	ixxun	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \to [A, B) \cup [B, C) = [A, C)$