Metamath Proof Explorer


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