iccintsng

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

		Ref	Expression
	Assertion	iccintsng	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐵 [,] 𝐶 ) ) = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		simpl1	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) ) → 𝐴 ∈ ℝ^* )
2		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) ) → 𝐵 ∈ ℝ^* )
3		simprl	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
4		iccleub	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ≤ 𝐵 )
5	1 2 3 4	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) ) → 𝑥 ≤ 𝐵 )
6		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) ) → 𝐶 ∈ ℝ^* )
7		simprr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) ) → 𝑥 ∈ ( 𝐵 [,] 𝐶 ) )
8		iccgelb	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) → 𝐵 ≤ 𝑥 )
9	2 6 7 8	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) ) → 𝐵 ≤ 𝑥 )
10		eliccxr	⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → 𝑥 ∈ ℝ^* )
11	3 10	syl	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) ) → 𝑥 ∈ ℝ^* )
12	11 2	jca	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) ) → ( 𝑥 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) )
13		xrletri3	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑥 = 𝐵 ↔ ( 𝑥 ≤ 𝐵 ∧ 𝐵 ≤ 𝑥 ) ) )
14	12 13	syl	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) ) → ( 𝑥 = 𝐵 ↔ ( 𝑥 ≤ 𝐵 ∧ 𝐵 ≤ 𝑥 ) ) )
15	5 9 14	mpbir2and	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) ) → 𝑥 = 𝐵 )
16	15	ex	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) → 𝑥 = 𝐵 ) )
17	16	adantr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) → 𝑥 = 𝐵 ) )
18		simpll1	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐴 ∈ ℝ^* )
19		simpll2	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ ℝ^* )
20		simplrl	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐴 ≤ 𝐵 )
21		simpr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
22		simpr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
23		ubicc2	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
24	23	adantr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
25	22 24	eqeltrd	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
26	18 19 20 21 25	syl31anc	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
27		simpll3	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐶 ∈ ℝ^* )
28		simplrr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐵 ≤ 𝐶 )
29		simpr	⊢ ( ( ( 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
30		lbicc2	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ 𝐵 ≤ 𝐶 ) → 𝐵 ∈ ( 𝐵 [,] 𝐶 ) )
31	30	adantr	⊢ ( ( ( 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ ( 𝐵 [,] 𝐶 ) )
32	29 31	eqeltrd	⊢ ( ( ( 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐵 [,] 𝐶 ) )
33	19 27 28 21 32	syl31anc	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐵 [,] 𝐶 ) )
34	26 33	jca	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) )
35	34	ex	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( 𝑥 = 𝐵 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) ) )
36	17 35	impbid	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) ↔ 𝑥 = 𝐵 ) )
37		elin	⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐵 [,] 𝐶 ) ) ↔ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) )
38		velsn	⊢ ( 𝑥 ∈ { 𝐵 } ↔ 𝑥 = 𝐵 )
39	36 37 38	3bitr4g	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐵 [,] 𝐶 ) ) ↔ 𝑥 ∈ { 𝐵 } ) )
40	39	eqrdv	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐵 [,] 𝐶 ) ) = { 𝐵 } )

Metamath Proof Explorer

Theorem iccintsng

Proof