prunioo

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

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

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \leq B$
2		xrleloe	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \leq B \leftrightarrow (A < B \lor A = B))$
3	2	3adant3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A \leq B \leftrightarrow (A < B \lor A = B))$
4		df-pr	$⊢ \{A, B\} = \{A\} \cup \{B\}$
5	4	uneq2i	$⊢ (A, B) \cup \{A, B\} = (A, B) \cup (\{A\} \cup \{B\})$
6		unass	$⊢ ((A, B) \cup \{A\}) \cup \{B\} = (A, B) \cup (\{A\} \cup \{B\})$
7	5 6	eqtr4i	$⊢ (A, B) \cup \{A, B\} = ((A, B) \cup \{A\}) \cup \{B\}$
8		uncom	$⊢ (A, B) \cup \{A\} = \{A\} \cup (A, B)$
9		snunioo	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \{A\} \cup (A, B) = [A, B)$
10	8 9	eqtrid	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (A, B) \cup \{A\} = [A, B)$
11	10	uneq1d	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to ((A, B) \cup \{A\}) \cup \{B\} = [A, B) \cup \{B\}$
12	7 11	eqtrid	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (A, B) \cup \{A, B\} = [A, B) \cup \{B\}$
13	12	3expa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to (A, B) \cup \{A, B\} = [A, B) \cup \{B\}$
14	13	3adantl3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land A < B) \to (A, B) \cup \{A, B\} = [A, B) \cup \{B\}$
15		snunico	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to [A, B) \cup \{B\} = [A, B]$
16	15	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land A < B) \to [A, B) \cup \{B\} = [A, B]$
17	14 16	eqtrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land A < B) \to (A, B) \cup \{A, B\} = [A, B]$
18	17	ex	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A < B \to (A, B) \cup \{A, B\} = [A, B])$
19		iccid	$⊢ A \in ℝ^{*} \to [A, A] = \{A\}$
20	19	3ad2ant1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to [A, A] = \{A\}$
21	20	eqcomd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to \{A\} = [A, A]$
22		uncom	$⊢ \emptyset \cup \{A\} = \{A\} \cup \emptyset$
23		un0	$⊢ \{A\} \cup \emptyset = \{A\}$
24	22 23	eqtri	$⊢ \emptyset \cup \{A\} = \{A\}$
25		iooid	$⊢ (A, A) = \emptyset$
26		oveq2	$⊢ A = B \to (A, A) = (A, B)$
27	25 26	eqtr3id	$⊢ A = B \to \emptyset = (A, B)$
28		dfsn2	$⊢ \{A\} = \{A, A\}$
29		preq2	$⊢ A = B \to \{A, A\} = \{A, B\}$
30	28 29	eqtrid	$⊢ A = B \to \{A\} = \{A, B\}$
31	27 30	uneq12d	$⊢ A = B \to \emptyset \cup \{A\} = (A, B) \cup \{A, B\}$
32	24 31	eqtr3id	$⊢ A = B \to \{A\} = (A, B) \cup \{A, B\}$
33		oveq2	$⊢ A = B \to [A, A] = [A, B]$
34	32 33	eqeq12d	$⊢ A = B \to (\{A\} = [A, A] \leftrightarrow (A, B) \cup \{A, B\} = [A, B])$
35	21 34	syl5ibcom	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A = B \to (A, B) \cup \{A, B\} = [A, B])$
36	18 35	jaod	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to ((A < B \lor A = B) \to (A, B) \cup \{A, B\} = [A, B])$
37	3 36	sylbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A \leq B \to (A, B) \cup \{A, B\} = [A, B])$
38	1 37	mpd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A, B) \cup \{A, B\} = [A, B]$

Metamath Proof Explorer

Theorem prunioo

Proof