Metamath Proof Explorer

Theorem iocinico

Description: The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019)

Ref Expression
Assertion iocinico 
|- ( ( ( 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 df-in 
 |-  ( ( A (,] B ) i^i ( B [,) C ) ) = { x | ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) }
2 elioc1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( x e. ( A (,] B ) <-> ( x e. RR* /\ A < x /\ x <_ B ) ) )
3 2 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( x e. ( A (,] B ) <-> ( x e. RR* /\ A < x /\ x <_ B ) ) )
4 3simpb 
 |-  ( ( x e. RR* /\ A < x /\ x <_ B ) -> ( x e. RR* /\ x <_ B ) )
5 3 4 biimtrdi 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( x e. ( A (,] B ) -> ( x e. RR* /\ x <_ B ) ) )
6 elico1 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( x e. ( B [,) C ) <-> ( x e. RR* /\ B <_ x /\ x < C ) ) )
7 6 3adant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( x e. ( B [,) C ) <-> ( x e. RR* /\ B <_ x /\ x < C ) ) )
8 3simpa 
 |-  ( ( x e. RR* /\ B <_ x /\ x < C ) -> ( x e. RR* /\ B <_ x ) )
9 7 8 biimtrdi 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( x e. ( B [,) C ) -> ( x e. RR* /\ B <_ x ) ) )
10 5 9 anim12d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) -> ( ( x e. RR* /\ x <_ B ) /\ ( x e. RR* /\ B <_ x ) ) ) )
11 simpll 
 |-  ( ( ( x e. RR* /\ x <_ B ) /\ ( x e. RR* /\ B <_ x ) ) -> x e. RR* )
12 simprr 
 |-  ( ( ( x e. RR* /\ x <_ B ) /\ ( x e. RR* /\ B <_ x ) ) -> B <_ x )
13 simplr 
 |-  ( ( ( x e. RR* /\ x <_ B ) /\ ( x e. RR* /\ B <_ x ) ) -> x <_ B )
14 11 12 13 3jca 
 |-  ( ( ( x e. RR* /\ x <_ B ) /\ ( x e. RR* /\ B <_ x ) ) -> ( x e. RR* /\ B <_ x /\ x <_ B ) )
15 10 14 syl6 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) -> ( x e. RR* /\ B <_ x /\ x <_ B ) ) )
16 elicc1 
 |-  ( ( B e. RR* /\ B e. RR* ) -> ( x e. ( B [,] B ) <-> ( x e. RR* /\ B <_ x /\ x <_ B ) ) )
17 16 anidms 
 |-  ( B e. RR* -> ( x e. ( B [,] B ) <-> ( x e. RR* /\ B <_ x /\ x <_ B ) ) )
18 17 3ad2ant2 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( x e. ( B [,] B ) <-> ( x e. RR* /\ B <_ x /\ x <_ B ) ) )
19 15 18 sylibrd 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) -> x e. ( B [,] B ) ) )
20 19 ss2abdv 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> { x | ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) } C_ { x | x e. ( B [,] B ) } )
21 1 20 eqsstrid 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A (,] B ) i^i ( B [,) C ) ) C_ { x | x e. ( B [,] B ) } )
22 abid2 
 |-  { x | x e. ( B [,] B ) } = ( B [,] B )
23 21 22 sseqtrdi 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A (,] B ) i^i ( B [,) C ) ) C_ ( B [,] B ) )
24 23 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,] B ) i^i ( B [,) C ) ) C_ ( B [,] B ) )
25 iccid 
 |-  ( B e. RR* -> ( B [,] B ) = { B } )
26 25 3ad2ant2 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( B [,] B ) = { B } )
27 26 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( B [,] B ) = { B } )
28 24 27 sseqtrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,] B ) i^i ( B [,) C ) ) C_ { B } )
29 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B e. RR* )
30 simprl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> A < B )
31 29 xrleidd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B <_ B )
32 elioc1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( B e. ( A (,] B ) <-> ( B e. RR* /\ A < B /\ B <_ B ) ) )
33 32 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( B e. ( A (,] B ) <-> ( B e. RR* /\ A < B /\ B <_ B ) ) )
34 33 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( B e. ( A (,] B ) <-> ( B e. RR* /\ A < B /\ B <_ B ) ) )
35 29 30 31 34 mpbir3and 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B e. ( A (,] B ) )
36 simprr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B < C )
37 elico1 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B e. ( B [,) C ) <-> ( B e. RR* /\ B <_ B /\ B < C ) ) )
38 37 3adant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( B e. ( B [,) C ) <-> ( B e. RR* /\ B <_ B /\ B < C ) ) )
39 38 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( B e. ( B [,) C ) <-> ( B e. RR* /\ B <_ B /\ B < C ) ) )
40 29 31 36 39 mpbir3and 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B e. ( B [,) C ) )
41 35 40 elind 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B e. ( ( A (,] B ) i^i ( B [,) C ) ) )
42 41 snssd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> { B } C_ ( ( A (,] B ) i^i ( B [,) C ) ) )
43 28 42 eqssd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,] B ) i^i ( B [,) C ) ) = { B } )