Theorem iccssico2

Description: Condition for a closed interval to be a subset of a closed-below, open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015)

	Ref	Expression
Assertion	iccssico2	|- ( ( C e. ( A [,) B ) /\ D e. ( A [,) 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	1	elmpocl1	|- ( C e. ( A [,) B ) -> A e. RR* )
3	2	adantr	|- ( ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) -> A e. RR* )
4	1	elmpocl2	|- ( C e. ( A [,) B ) -> B e. RR* )
5	4	adantr	|- ( ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) -> B e. RR* )
6	1	elixx3g	|- ( C e. ( A [,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A <_ C /\ C < B ) ) )
7	6	simprbi	|- ( C e. ( A [,) B ) -> ( A <_ C /\ C < B ) )
8	7	simpld	|- ( C e. ( A [,) B ) -> A <_ C )
9	8	adantr	|- ( ( 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		iccssico	|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D < B ) ) -> ( C [,] D ) C_ ( A [,) B ) )
15	3 5 9 13 14	syl22anc	|- ( ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) -> ( C [,] D ) C_ ( A [,) B ) )