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

Metamath Proof Explorer

Theorem joiniooico

Description: Disjoint joining an open interval with a closed-below, open-above interval to form a closed-below, open-above interval. (Contributed by Thierry Arnoux, 26-Sep-2017)

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

Proof

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		xrlenlt	$⊢ (B \in ℝ^{} \land w \in ℝ^{}) \to (B \leq w \leftrightarrow \neg w < B)$
4	1 2 3	ixxdisj	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A, B) \cap [B, C) = \emptyset$
5	4	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B \leq C)) \to (A, B) \cap [B, C) = \emptyset$
6		xrltletr	$⊢ (w \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((w < B \land B \leq C) \to w < C)$
7		xrltletr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land w \in ℝ^{*}) \to ((A < B \land B \leq w) \to A < w)$
8	1 2 3 1 6 7	ixxun	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B \leq C)) \to (A, B) \cup [B, C) = (A, C)$
9	5 8	jca	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B \leq C)) \to ((A, B) \cap [B, C) = \emptyset \land (A, B) \cup [B, C) = (A, C))$