Metamath Proof Explorer

Theorem iocunico

Description: Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019)

Ref Expression
Assertion iocunico 
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,] B ) u. ( B [,) C ) ) = ( A (,) C ) )

Proof

Step Hyp Ref Expression
1 un23 
 |-  ( ( ( A (,) B ) u. { B } ) u. ( B (,) C ) ) = ( ( ( A (,) B ) u. ( B (,) C ) ) u. { B } )
2 unundir 
 |-  ( ( ( A (,) B ) u. ( B (,) C ) ) u. { B } ) = ( ( ( A (,) B ) u. { B } ) u. ( ( B (,) C ) u. { B } ) )
3 uncom 
 |-  ( ( B (,) C ) u. { B } ) = ( { B } u. ( B (,) C ) )
4 3 uneq2i 
 |-  ( ( ( A (,) B ) u. { B } ) u. ( ( B (,) C ) u. { B } ) ) = ( ( ( A (,) B ) u. { B } ) u. ( { B } u. ( B (,) C ) ) )
5 1 2 4 3eqtrri 
 |-  ( ( ( A (,) B ) u. { B } ) u. ( { B } u. ( B (,) C ) ) ) = ( ( ( A (,) B ) u. { B } ) u. ( B (,) C ) )
6 simpl1 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> A e. RR* )
7 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B e. RR* )
8 simprl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> A < B )
9 ioounsn 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
10 6 7 8 9 syl3anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
11 simpl3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> C e. RR* )
12 simprr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B < C )
13 snunioo 
 |-  ( ( B e. RR* /\ C e. RR* /\ B < C ) -> ( { B } u. ( B (,) C ) ) = ( B [,) C ) )
14 7 11 12 13 syl3anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( { B } u. ( B (,) C ) ) = ( B [,) C ) )
15 10 14 uneq12d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( ( A (,) B ) u. { B } ) u. ( { B } u. ( B (,) C ) ) ) = ( ( A (,] B ) u. ( B [,) C ) ) )
16 ioojoin 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( ( A (,) B ) u. { B } ) u. ( B (,) C ) ) = ( A (,) C ) )
17 5 15 16 3eqtr3a 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,] B ) u. ( B [,) C ) ) = ( A (,) C ) )