icoiccdif

Description: Left-closed right-open interval gotten by a closed iterval taking away the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		icossicc	$⊢ [A, B) \subseteq [A, B]$
2	1	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to [A, B) \subseteq [A, B]$
3	2	sselda	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in [A, B)) \to x \in [A, B]$
4		elico1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (x \in [A, B) \leftrightarrow (x \in ℝ^{*} \land A \leq x \land x < B))$
5	4	biimpa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in [A, B)) \to (x \in ℝ^{*} \land A \leq x \land x < B)$
6	5	simp1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in [A, B)) \to x \in ℝ^{*}$
7		simplr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in [A, B)) \to B \in ℝ^{*}$
8	5	simp3d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in [A, B)) \to x < B$
9		xrltne	$⊢ (x \in ℝ^{} \land B \in ℝ^{} \land x < B) \to B \neq x$
10	6 7 8 9	syl3anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in [A, B)) \to B \neq x$
11	10	necomd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in [A, B)) \to x \neq B$
12	11	neneqd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in [A, B)) \to \neg x = B$
13		velsn	$⊢ x \in \{B\} \leftrightarrow x = B$
14	12 13	sylnibr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in [A, B)) \to \neg x \in \{B\}$
15	3 14	eldifd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in [A, B)) \to x \in ([A, B] ∖ \{B\})$
16	15	ex	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (x \in [A, B) \to x \in ([A, B] ∖ \{B\}))$
17	16	ssrdv	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to [A, B) \subseteq [A, B] ∖ \{B\}$
18		simpll	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ([A, B] ∖ \{B\})) \to A \in ℝ^{*}$
19		simplr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ([A, B] ∖ \{B\})) \to B \in ℝ^{*}$
20		eldifi	$⊢ x \in ([A, B] ∖ \{B\}) \to x \in [A, B]$
21		eliccxr	$⊢ x \in [A, B] \to x \in ℝ^{*}$
22	20 21	syl	$⊢ x \in ([A, B] ∖ \{B\}) \to x \in ℝ^{*}$
23	22	adantl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ([A, B] ∖ \{B\})) \to x \in ℝ^{*}$
24	20	adantl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ([A, B] ∖ \{B\})) \to x \in [A, B]$
25		elicc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (x \in [A, B] \leftrightarrow (x \in ℝ^{*} \land A \leq x \land x \leq B))$
26	25	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ([A, B] ∖ \{B\})) \to (x \in [A, B] \leftrightarrow (x \in ℝ^{*} \land A \leq x \land x \leq B))$
27	24 26	mpbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ([A, B] ∖ \{B\})) \to (x \in ℝ^{*} \land A \leq x \land x \leq B)$
28	27	simp2d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ([A, B] ∖ \{B\})) \to A \leq x$
29		eldifsni	$⊢ x \in ([A, B] ∖ \{B\}) \to x \neq B$
30	29	necomd	$⊢ x \in ([A, B] ∖ \{B\}) \to B \neq x$
31	30	adantl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ([A, B] ∖ \{B\})) \to B \neq x$
32	27	simp3d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ([A, B] ∖ \{B\})) \to x \leq B$
33		xrleltne	$⊢ (x \in ℝ^{} \land B \in ℝ^{} \land x \leq B) \to (x < B \leftrightarrow B \neq x)$
34	23 19 32 33	syl3anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ([A, B] ∖ \{B\})) \to (x < B \leftrightarrow B \neq x)$
35	31 34	mpbird	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ([A, B] ∖ \{B\})) \to x < B$
36	18 19 23 28 35	elicod	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ([A, B] ∖ \{B\})) \to x \in [A, B)$
37	17 36	eqelssd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to [A, B) = [A, B] ∖ \{B\}$

Metamath Proof Explorer

Theorem icoiccdif

Proof