Metamath Proof Explorer

Theorem ioojoin

Description: Join two open intervals to create a third. (Contributed by NM, 11-Aug-2008) (Proof shortened by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion ioojoin 
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( ( A (,) B ) u. { B } ) u. ( B (,) C ) ) = ( A (,) C ) )

Proof

Step Hyp Ref Expression
1 unass 
 |-  ( ( ( A (,) B ) u. { B } ) u. ( B (,) C ) ) = ( ( A (,) B ) u. ( { B } u. ( B (,) C ) ) )
2 snunioo 
 |-  ( ( B e. RR* /\ C e. RR* /\ B < C ) -> ( { B } u. ( B (,) C ) ) = ( B [,) C ) )
3 2 3expa 
 |-  ( ( ( B e. RR* /\ C e. RR* ) /\ B < C ) -> ( { B } u. ( B (,) C ) ) = ( B [,) C ) )
4 3 3adantl1 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ B < C ) -> ( { B } u. ( B (,) C ) ) = ( B [,) C ) )
5 4 adantrl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( { B } u. ( B (,) C ) ) = ( B [,) C ) )
6 5 uneq2d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,) B ) u. ( { B } u. ( B (,) C ) ) ) = ( ( A (,) B ) u. ( B [,) C ) ) )
7 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
8 df-ico 
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
9 xrlenlt 
 |-  ( ( B e. RR* /\ w e. RR* ) -> ( B <_ w <-> -. w < B ) )
10 xrlttr 
 |-  ( ( w e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( w < B /\ B < C ) -> w < C ) )
11 xrltletr 
 |-  ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) -> ( ( A < B /\ B <_ w ) -> A < w ) )
12 7 8 9 7 10 11 ixxun 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,) B ) u. ( B [,) C ) ) = ( A (,) C ) )
13 6 12 eqtrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,) B ) u. ( { B } u. ( B (,) C ) ) ) = ( A (,) C ) )
14 1 13 eqtrid 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( ( A (,) B ) u. { B } ) u. ( B (,) C ) ) = ( A (,) C ) )