iccintsng

Description: Intersection of two adiacent closed intervals is a singleton. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	iccintsng	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \to [A, B] \cap [B, C] = \{B\}$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (x \in [A, B] \land x \in [B, C])) \to A \in ℝ^{}$
2		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (x \in [A, B] \land x \in [B, C])) \to B \in ℝ^{}$
3		simprl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (x \in [A, B] \land x \in [B, C])) \to x \in [A, B]$
4		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in [A, B]) \to x \leq B$
5	1 2 3 4	syl3anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (x \in [A, B] \land x \in [B, C])) \to x \leq B$
6		simpl3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (x \in [A, B] \land x \in [B, C])) \to C \in ℝ^{}$
7		simprr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (x \in [A, B] \land x \in [B, C])) \to x \in [B, C]$
8		iccgelb	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land x \in [B, C]) \to B \leq x$
9	2 6 7 8	syl3anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (x \in [A, B] \land x \in [B, C])) \to B \leq x$
10		eliccxr	$⊢ x \in [A, B] \to x \in ℝ^{*}$
11	3 10	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (x \in [A, B] \land x \in [B, C])) \to x \in ℝ^{}$
12	11 2	jca	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (x \in [A, B] \land x \in [B, C])) \to (x \in ℝ^{} \land B \in ℝ^{*})$
13		xrletri3	$⊢ (x \in ℝ^{} \land B \in ℝ^{}) \to (x = B \leftrightarrow (x \leq B \land B \leq x))$
14	12 13	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (x \in [A, B] \land x \in [B, C])) \to (x = B \leftrightarrow (x \leq B \land B \leq x))$
15	5 9 14	mpbir2and	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (x \in [A, B] \land x \in [B, C])) \to x = B$
16	15	ex	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((x \in [A, B] \land x \in [B, C]) \to x = B)$
17	16	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \to ((x \in [A, B] \land x \in [B, C]) \to x = B)$
18		simpll1	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A \leq B \land B \leq C)) \land x = B) \to A \in ℝ^{}$
19		simpll2	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A \leq B \land B \leq C)) \land x = B) \to B \in ℝ^{}$
20		simplrl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \land x = B) \to A \leq B$
21		simpr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \land x = B) \to x = B$
22		simpr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land x = B) \to x = B$
23		ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$
24	23	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land x = B) \to B \in [A, B]$
25	22 24	eqeltrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \land x = B) \to x \in [A, B]$
26	18 19 20 21 25	syl31anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \land x = B) \to x \in [A, B]$
27		simpll3	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A \leq B \land B \leq C)) \land x = B) \to C \in ℝ^{}$
28		simplrr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \land x = B) \to B \leq C$
29		simpr	$⊢ ((B \in ℝ^{} \land C \in ℝ^{} \land B \leq C) \land x = B) \to x = B$
30		lbicc2	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land B \leq C) \to B \in [B, C]$
31	30	adantr	$⊢ ((B \in ℝ^{} \land C \in ℝ^{} \land B \leq C) \land x = B) \to B \in [B, C]$
32	29 31	eqeltrd	$⊢ ((B \in ℝ^{} \land C \in ℝ^{} \land B \leq C) \land x = B) \to x \in [B, C]$
33	19 27 28 21 32	syl31anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \land x = B) \to x \in [B, C]$
34	26 33	jca	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \land x = B) \to (x \in [A, B] \land x \in [B, C])$
35	34	ex	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \to (x = B \to (x \in [A, B] \land x \in [B, C]))$
36	17 35	impbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \to ((x \in [A, B] \land x \in [B, C]) \leftrightarrow x = B)$
37		elin	$⊢ x \in ([A, B] \cap [B, C]) \leftrightarrow (x \in [A, B] \land x \in [B, C])$
38		velsn	$⊢ x \in \{B\} \leftrightarrow x = B$
39	36 37 38	3bitr4g	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \to (x \in ([A, B] \cap [B, C]) \leftrightarrow x \in \{B\})$
40	39	eqrdv	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq B \land B \leq C)) \to [A, B] \cap [B, C] = \{B\}$

Metamath Proof Explorer

Theorem iccintsng

Proof