Theorem iccssico

Description: Condition for a closed interval to be a subset of a half-open interval. (Contributed by Mario Carneiro, 9-Sep-2015)

	Ref	Expression
Assertion	iccssico	|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D < B ) ) -> ( C [,] D ) C_ ( A [,) B ) )

Proof

Step	Hyp	Ref	Expression
1		df-ico	|- [,) = ( 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		xrletr	|- ( ( 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 ) )