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

Metamath Proof Explorer

Theorem snunioo

Description: The closure of one end of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008) (Proof shortened by Mario Carneiro, 16-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to A \in ℝ^{*}$
2		iccid	$⊢ A \in ℝ^{*} \to [A, A] = \{A\}$
3	1 2	syl	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to [A, A] = \{A\}$
4	3	uneq1d	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to [A, A] \cup (A, B) = \{A\} \cup (A, B)$
5		simp2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to B \in ℝ^{*}$
6	1	xrleidd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to A \leq A$
7		simp3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to A < B$
8		df-icc	$⊢ [.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\})$
9		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
10		xrltnle	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A < w \leftrightarrow \neg w \leq A)$
11		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
12		xrlelttr	$⊢ (w \in ℝ^{} \land A \in ℝ^{} \land B \in ℝ^{*}) \to ((w \leq A \land A < B) \to w < B)$
13		xrltle	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A < w \to A \leq w)$
14	13	3adant1	$⊢ (A \in ℝ^{} \land A \in ℝ^{} \land w \in ℝ^{*}) \to (A < w \to A \leq w)$
15	14	adantld	$⊢ (A \in ℝ^{} \land A \in ℝ^{} \land w \in ℝ^{*}) \to ((A \leq A \land A < w) \to A \leq w)$
16	8 9 10 11 12 15	ixxun	$⊢ ((A \in ℝ^{} \land A \in ℝ^{} \land B \in ℝ^{*}) \land (A \leq A \land A < B)) \to [A, A] \cup (A, B) = [A, B)$
17	1 1 5 6 7 16	syl32anc	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to [A, A] \cup (A, B) = [A, B)$
18	4 17	eqtr3d	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \{A\} \cup (A, B) = [A, B)$