Step |
Hyp |
Ref |
Expression |
1 |
|
df-icc |
|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } ) |
2 |
1
|
elixx3g |
|- ( C e. ( A [,] B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A <_ C /\ C <_ B ) ) ) |
3 |
2
|
simplbi |
|- ( C e. ( A [,] B ) -> ( A e. RR* /\ B e. RR* /\ C e. RR* ) ) |
4 |
3
|
adantr |
|- ( ( C e. ( A [,] B ) /\ D e. ( A [,] B ) ) -> ( A e. RR* /\ B e. RR* /\ C e. RR* ) ) |
5 |
4
|
simp1d |
|- ( ( C e. ( A [,] B ) /\ D e. ( A [,] B ) ) -> A e. RR* ) |
6 |
4
|
simp2d |
|- ( ( C e. ( A [,] B ) /\ D e. ( A [,] B ) ) -> B e. RR* ) |
7 |
2
|
simprbi |
|- ( C e. ( A [,] B ) -> ( A <_ C /\ C <_ B ) ) |
8 |
7
|
adantr |
|- ( ( C e. ( A [,] B ) /\ D e. ( A [,] B ) ) -> ( A <_ C /\ C <_ B ) ) |
9 |
8
|
simpld |
|- ( ( C e. ( A [,] B ) /\ D e. ( A [,] B ) ) -> A <_ C ) |
10 |
1
|
elixx3g |
|- ( D e. ( A [,] B ) <-> ( ( A e. RR* /\ B e. RR* /\ D e. RR* ) /\ ( A <_ D /\ D <_ B ) ) ) |
11 |
10
|
simprbi |
|- ( D e. ( A [,] B ) -> ( A <_ D /\ D <_ B ) ) |
12 |
11
|
simprd |
|- ( D e. ( A [,] B ) -> D <_ B ) |
13 |
12
|
adantl |
|- ( ( C e. ( A [,] B ) /\ D e. ( A [,] B ) ) -> D <_ B ) |
14 |
|
xrletr |
|- ( ( A e. RR* /\ C e. RR* /\ w e. RR* ) -> ( ( A <_ C /\ C <_ w ) -> A <_ w ) ) |
15 |
|
xrletr |
|- ( ( w e. RR* /\ D e. RR* /\ B e. RR* ) -> ( ( w <_ D /\ D <_ B ) -> w <_ B ) ) |
16 |
1 1 14 15
|
ixxss12 |
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D <_ B ) ) -> ( C [,] D ) C_ ( A [,] B ) ) |
17 |
5 6 9 13 16
|
syl22anc |
|- ( ( C e. ( A [,] B ) /\ D e. ( A [,] B ) ) -> ( C [,] D ) C_ ( A [,] B ) ) |