snunioc

Description: The closure of the open end of a left-open real interval. (Contributed by Thierry Arnoux, 28-Mar-2017)

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

Proof

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

Metamath Proof Explorer

Theorem snunioc

Proof