Metamath Proof Explorer

Theorem ioojoin

Description: Join two open intervals to create a third. (Contributed by NM, 11-Aug-2008) (Proof shortened by Mario Carneiro, 16-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		unass	$⊢ ((A, B) \cup \{B\}) \cup (B, C) = (A, B) \cup (\{B\} \cup (B, C))$
2		snunioo	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land B < C) \to \{B\} \cup (B, C) = [B, C)$
3	2	3expa	$⊢ ((B \in ℝ^{} \land C \in ℝ^{}) \land B < C) \to \{B\} \cup (B, C) = [B, C)$
4	3	3adantl1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land B < C) \to \{B\} \cup (B, C) = [B, C)$
5	4	adantrl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to \{B\} \cup (B, C) = [B, C)$
6	5	uneq2d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to (A, B) \cup (\{B\} \cup (B, C)) = (A, B) \cup [B, C)$
7		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
8		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
9		xrlenlt	$⊢ (B \in ℝ^{} \land w \in ℝ^{}) \to (B \leq w \leftrightarrow \neg w < B)$
10		xrlttr	$⊢ (w \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((w < B \land B < C) \to w < C)$
11		xrltletr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land w \in ℝ^{*}) \to ((A < B \land B \leq w) \to A < w)$
12	7 8 9 7 10 11	ixxun	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to (A, B) \cup [B, C) = (A, C)$
13	6 12	eqtrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to (A, B) \cup (\{B\} \cup (B, C)) = (A, C)$
14	1 13	eqtrid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to ((A, B) \cup \{B\}) \cup (B, C) = (A, C)$