Description: Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | iccssioo | |- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A < C /\ D < B ) ) -> ( C [,] D ) C_ ( A (,) B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ioo | |- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } ) |
|
2 | df-icc | |- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } ) |
|
3 | xrltletr | |- ( ( A e. RR* /\ C e. RR* /\ w e. RR* ) -> ( ( A < C /\ C <_ w ) -> A < w ) ) |
|
4 | xrlelttr | |- ( ( w e. RR* /\ D e. RR* /\ B e. RR* ) -> ( ( w <_ D /\ D < B ) -> w < B ) ) |
|
5 | 1 2 3 4 | ixxss12 | |- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A < C /\ D < B ) ) -> ( C [,] D ) C_ ( A (,) B ) ) |