Metamath Proof Explorer

Theorem iocinioc2

Description: Intersection between two open-below, closed-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 7-Aug-2017)

Ref Expression
Assertion iocinioc2 
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( ( A (,] C ) i^i ( B (,] C ) ) = ( B (,] C ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( x e. ( ( A (,] C ) i^i ( B (,] C ) ) <-> ( x e. ( A (,] C ) /\ x e. ( B (,] C ) ) )
2 simpl1 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> A e. RR* )
3 simpl3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> C e. RR* )
4 elioc1 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( x e. ( A (,] C ) <-> ( x e. RR* /\ A < x /\ x <_ C ) ) )
5 2 3 4 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( x e. ( A (,] C ) <-> ( x e. RR* /\ A < x /\ x <_ C ) ) )
6 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> B e. RR* )
7 elioc1 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( x e. ( B (,] C ) <-> ( x e. RR* /\ B < x /\ x <_ C ) ) )
8 6 3 7 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( x e. ( B (,] C ) <-> ( x e. RR* /\ B < x /\ x <_ C ) ) )
9 5 8 anbi12d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( ( x e. ( A (,] C ) /\ x e. ( B (,] C ) ) <-> ( ( x e. RR* /\ A < x /\ x <_ C ) /\ ( x e. RR* /\ B < x /\ x <_ C ) ) ) )
10 simp31 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B /\ ( x e. RR* /\ B < x /\ x <_ C ) ) -> x e. RR* )
11 2 3adant3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B /\ ( x e. RR* /\ B < x /\ x <_ C ) ) -> A e. RR* )
12 6 3adant3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B /\ ( x e. RR* /\ B < x /\ x <_ C ) ) -> B e. RR* )
13 simp2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B /\ ( x e. RR* /\ B < x /\ x <_ C ) ) -> A <_ B )
14 simp32 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B /\ ( x e. RR* /\ B < x /\ x <_ C ) ) -> B < x )
15 11 12 10 13 14 xrlelttrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B /\ ( x e. RR* /\ B < x /\ x <_ C ) ) -> A < x )
16 simp33 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B /\ ( x e. RR* /\ B < x /\ x <_ C ) ) -> x <_ C )
17 10 15 16 3jca 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B /\ ( x e. RR* /\ B < x /\ x <_ C ) ) -> ( x e. RR* /\ A < x /\ x <_ C ) )
18 17 3expia 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( ( x e. RR* /\ B < x /\ x <_ C ) -> ( x e. RR* /\ A < x /\ x <_ C ) ) )
19 18 pm4.71rd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( ( x e. RR* /\ B < x /\ x <_ C ) <-> ( ( x e. RR* /\ A < x /\ x <_ C ) /\ ( x e. RR* /\ B < x /\ x <_ C ) ) ) )
20 9 19 bitr4d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( ( x e. ( A (,] C ) /\ x e. ( B (,] C ) ) <-> ( x e. RR* /\ B < x /\ x <_ C ) ) )
21 1 20 syl5bb 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( x e. ( ( A (,] C ) i^i ( B (,] C ) ) <-> ( x e. RR* /\ B < x /\ x <_ C ) ) )
22 21 8 bitr4d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( x e. ( ( A (,] C ) i^i ( B (,] C ) ) <-> x e. ( B (,] C ) ) )
23 22 eqrdv 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( ( A (,] C ) i^i ( B (,] C ) ) = ( B (,] C ) )