Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
|- ( ( A e. RR* /\ D e. RR* /\ B < C ) -> A e. RR* ) |
2 |
|
simp3 |
|- ( ( A e. RR* /\ D e. RR* /\ B < C ) -> B < C ) |
3 |
|
ltrelxr |
|- < C_ ( RR* X. RR* ) |
4 |
3
|
brel |
|- ( B < C -> ( B e. RR* /\ C e. RR* ) ) |
5 |
2 4
|
syl |
|- ( ( A e. RR* /\ D e. RR* /\ B < C ) -> ( B e. RR* /\ C e. RR* ) ) |
6 |
5
|
simprd |
|- ( ( A e. RR* /\ D e. RR* /\ B < C ) -> C e. RR* ) |
7 |
1
|
xrleidd |
|- ( ( A e. RR* /\ D e. RR* /\ B < C ) -> A <_ A ) |
8 |
|
iccssico |
|- ( ( ( A e. RR* /\ C e. RR* ) /\ ( A <_ A /\ B < C ) ) -> ( A [,] B ) C_ ( A [,) C ) ) |
9 |
1 6 7 2 8
|
syl22anc |
|- ( ( A e. RR* /\ D e. RR* /\ B < C ) -> ( A [,] B ) C_ ( A [,) C ) ) |
10 |
|
simp2 |
|- ( ( A e. RR* /\ D e. RR* /\ B < C ) -> D e. RR* ) |
11 |
|
df-ico |
|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } ) |
12 |
|
df-icc |
|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } ) |
13 |
|
xrlenlt |
|- ( ( C e. RR* /\ w e. RR* ) -> ( C <_ w <-> -. w < C ) ) |
14 |
11 12 13
|
ixxdisj |
|- ( ( A e. RR* /\ C e. RR* /\ D e. RR* ) -> ( ( A [,) C ) i^i ( C [,] D ) ) = (/) ) |
15 |
1 6 10 14
|
syl3anc |
|- ( ( A e. RR* /\ D e. RR* /\ B < C ) -> ( ( A [,) C ) i^i ( C [,] D ) ) = (/) ) |
16 |
9 15
|
ssdisjd |
|- ( ( A e. RR* /\ D e. RR* /\ B < C ) -> ( ( A [,] B ) i^i ( C [,] D ) ) = (/) ) |