Metamath Proof Explorer

Theorem joiniooico

Description: Disjoint joining an open interval with a closed-below, open-above interval to form a closed-below, open-above interval. (Contributed by Thierry Arnoux, 26-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 df-ioo 
 |-  (,) = ( a e. RR* , b e. RR* |-> { x e. RR* | ( a < x /\ x < b ) } )
2 df-ico 
 |-  [,) = ( a e. RR* , b e. RR* |-> { x e. RR* | ( a <_ x /\ x < b ) } )
3 xrlenlt 
 |-  ( ( B e. RR* /\ w e. RR* ) -> ( B <_ w <-> -. w < B ) )
4 1 2 3 ixxdisj 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A (,) B ) i^i ( B [,) C ) ) = (/) )
5 4 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B <_ C ) ) -> ( ( A (,) B ) i^i ( B [,) C ) ) = (/) )
6 xrltletr 
 |-  ( ( w e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( w < B /\ B <_ C ) -> w < C ) )
7 xrltletr 
 |-  ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) -> ( ( A < B /\ B <_ w ) -> A < w ) )
8 1 2 3 1 6 7 ixxun 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B <_ C ) ) -> ( ( A (,) B ) u. ( B [,) C ) ) = ( A (,) C ) )
9 5 8 jca 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B <_ C ) ) -> ( ( ( A (,) B ) i^i ( B [,) C ) ) = (/) /\ ( ( A (,) B ) u. ( B [,) C ) ) = ( A (,) C ) ) )