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