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 
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A <_ B /\ B <_ C ) ) -> ( ( A [,] B ) i^i ( B [,] C ) ) = { B } )

Proof

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