iccdifprioo

Description: An open interval is the closed interval without the bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		prunioo	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A, B) \cup \{A, B\} = [A, B]$
2	1	eqcomd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to [A, B] = (A, B) \cup \{A, B\}$
3	2	difeq1d	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to [A, B] ∖ \{A, B\} = ((A, B) \cup \{A, B\}) ∖ \{A, B\}$
4		difun2	$⊢ ((A, B) \cup \{A, B\}) ∖ \{A, B\} = (A, B) ∖ \{A, B\}$
5		iooinlbub	$⊢ (A, B) \cap \{A, B\} = \emptyset$
6		disj3	$⊢ (A, B) \cap \{A, B\} = \emptyset \leftrightarrow (A, B) = (A, B) ∖ \{A, B\}$
7	5 6	mpbi	$⊢ (A, B) = (A, B) ∖ \{A, B\}$
8	4 7	eqtr4i	$⊢ ((A, B) \cup \{A, B\}) ∖ \{A, B\} = (A, B)$
9	3 8	syl6eq	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to [A, B] ∖ \{A, B\} = (A, B)$
10	9	3expa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A \leq B) \to [A, B] ∖ \{A, B\} = (A, B)$
11		difssd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to [A, B] ∖ \{A, B\} \subseteq [A, B]$
12		simpr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to \neg A \leq B$
13		xrlenlt	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \leq B \leftrightarrow \neg B < A)$
14	13	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to (A \leq B \leftrightarrow \neg B < A)$
15	12 14	mtbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to \neg \neg B < A$
16	15	notnotrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to B < A$
17		icc0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B] = \emptyset \leftrightarrow B < A)$
18	17	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to ([A, B] = \emptyset \leftrightarrow B < A)$
19	16 18	mpbird	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to [A, B] = \emptyset$
20	11 19	sseqtrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to [A, B] ∖ \{A, B\} \subseteq \emptyset$
21		ss0	$⊢ [A, B] ∖ \{A, B\} \subseteq \emptyset \to [A, B] ∖ \{A, B\} = \emptyset$
22	20 21	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to [A, B] ∖ \{A, B\} = \emptyset$
23		simplr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to B \in ℝ^{*}$
24		simpll	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to A \in ℝ^{*}$
25	23 24 16	xrltled	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to B \leq A$
26		ioo0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B) = \emptyset \leftrightarrow B \leq A)$
27	26	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to ((A, B) = \emptyset \leftrightarrow B \leq A)$
28	25 27	mpbird	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to (A, B) = \emptyset$
29	22 28	eqtr4d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A \leq B) \to [A, B] ∖ \{A, B\} = (A, B)$
30	10 29	pm2.61dan	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to [A, B] ∖ \{A, B\} = (A, B)$

Metamath Proof Explorer

Theorem iccdifprioo

Proof