Step |
Hyp |
Ref |
Expression |
1 |
|
iooss1 |
|- ( ( B e. RR* /\ B <_ C ) -> ( C (,) D ) C_ ( B (,) D ) ) |
2 |
1
|
ad4ant24 |
|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B <_ C ) -> ( C (,) D ) C_ ( B (,) D ) ) |
3 |
|
ioossicc |
|- ( B (,) D ) C_ ( B [,] D ) |
4 |
2 3
|
sstrdi |
|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B <_ C ) -> ( C (,) D ) C_ ( B [,] D ) ) |
5 |
|
sslin |
|- ( ( C (,) D ) C_ ( B [,] D ) -> ( ( A (,) B ) i^i ( C (,) D ) ) C_ ( ( A (,) B ) i^i ( B [,] D ) ) ) |
6 |
4 5
|
syl |
|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B <_ C ) -> ( ( A (,) B ) i^i ( C (,) D ) ) C_ ( ( A (,) B ) i^i ( B [,] D ) ) ) |
7 |
|
simplll |
|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B <_ C ) -> A e. RR* ) |
8 |
|
simpllr |
|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B <_ C ) -> B e. RR* ) |
9 |
|
simplrr |
|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B <_ C ) -> D e. RR* ) |
10 |
|
df-ioo |
|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } ) |
11 |
|
df-icc |
|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } ) |
12 |
|
xrlenlt |
|- ( ( B e. RR* /\ w e. RR* ) -> ( B <_ w <-> -. w < B ) ) |
13 |
10 11 12
|
ixxdisj |
|- ( ( A e. RR* /\ B e. RR* /\ D e. RR* ) -> ( ( A (,) B ) i^i ( B [,] D ) ) = (/) ) |
14 |
7 8 9 13
|
syl3anc |
|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B <_ C ) -> ( ( A (,) B ) i^i ( B [,] D ) ) = (/) ) |
15 |
6 14
|
sseqtrd |
|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B <_ C ) -> ( ( A (,) B ) i^i ( C (,) D ) ) C_ (/) ) |
16 |
|
ss0 |
|- ( ( ( A (,) B ) i^i ( C (,) D ) ) C_ (/) -> ( ( A (,) B ) i^i ( C (,) D ) ) = (/) ) |
17 |
15 16
|
syl |
|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B <_ C ) -> ( ( A (,) B ) i^i ( C (,) D ) ) = (/) ) |