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 ) ) |