snunioo1

Description: The closure of one end of an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		uncom	$⊢ (A, B) \cup [A, A] = [A, A] \cup (A, B)$
2		iccid	$⊢ A \in ℝ^{*} \to [A, A] = \{A\}$
3	2	3ad2ant1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to [A, A] = \{A\}$
4	3	uneq2d	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (A, B) \cup [A, A] = (A, B) \cup \{A\}$
5		simp1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to A \in ℝ^{*}$
6		simp2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to B \in ℝ^{*}$
7		xrleid	$⊢ A \in ℝ^{*} \to A \leq A$
8	7	3ad2ant1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to A \leq A$
9		simp3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to A < B$
10		df-icc	$⊢ [.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\})$
11		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
12		xrltnle	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A < w \leftrightarrow \neg w \leq A)$
13		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
14		xrlelttr	$⊢ (w \in ℝ^{} \land A \in ℝ^{} \land B \in ℝ^{*}) \to ((w \leq A \land A < B) \to w < B)$
15		simpl1	$⊢ ((A \in ℝ^{} \land A \in ℝ^{} \land w \in ℝ^{}) \land (A \leq A \land A < w)) \to A \in ℝ^{}$
16		simpl3	$⊢ ((A \in ℝ^{} \land A \in ℝ^{} \land w \in ℝ^{}) \land (A \leq A \land A < w)) \to w \in ℝ^{}$
17		simprr	$⊢ ((A \in ℝ^{} \land A \in ℝ^{} \land w \in ℝ^{*}) \land (A \leq A \land A < w)) \to A < w$
18	15 16 17	xrltled	$⊢ ((A \in ℝ^{} \land A \in ℝ^{} \land w \in ℝ^{*}) \land (A \leq A \land A < w)) \to A \leq w$
19	18	ex	$⊢ (A \in ℝ^{} \land A \in ℝ^{} \land w \in ℝ^{*}) \to ((A \leq A \land A < w) \to A \leq w)$
20	10 11 12 13 14 19	ixxun	$⊢ ((A \in ℝ^{} \land A \in ℝ^{} \land B \in ℝ^{*}) \land (A \leq A \land A < B)) \to [A, A] \cup (A, B) = [A, B)$
21	5 5 6 8 9 20	syl32anc	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to [A, A] \cup (A, B) = [A, B)$
22	1 4 21	3eqtr3a	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (A, B) \cup \{A\} = [A, B)$

Metamath Proof Explorer

Theorem snunioo1

Proof