Theorem iccss2

Description: Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	iccss2	|- ( ( C e. ( A [,] B ) /\ D e. ( A [,] B ) ) -> ( C [,] D ) C_ ( A [,] B ) )

Proof

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 ) )