Theorem icossioo

Description: Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017)

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

Proof

Step	Hyp	Ref	Expression
1		df-ioo	|- (,) = ( a e. RR* , b e. RR* |-> { x e. RR* | ( a < x /\ x < b ) } )
2		df-ico	|- [,) = ( a e. RR* , b e. RR* |-> { x e. RR* | ( a <_ x /\ x < b ) } )
3		xrltletr	|- ( ( A e. RR* /\ C e. RR* /\ w e. RR* ) -> ( ( A < C /\ C <_ w ) -> A < w ) )
4		xrltletr	|- ( ( 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 ) )