Metamath Proof Explorer


Theorem 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 ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ ( 𝐴𝐵𝐵𝐶 ) ) → ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐵 [,] 𝐶 ) ) = { 𝐵 } )