Metamath Proof Explorer


Theorem iccss

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, 20-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 rexr
 |-  ( A e. RR -> A e. RR* )
2 rexr
 |-  ( B e. RR -> B e. RR* )
3 1 2 anim12i
 |-  ( ( A e. RR /\ B e. RR ) -> ( A e. RR* /\ B e. RR* ) )
4 df-icc
 |-  [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
5 xrletr
 |-  ( ( A e. RR* /\ C e. RR* /\ w e. RR* ) -> ( ( A <_ C /\ C <_ w ) -> A <_ w ) )
6 xrletr
 |-  ( ( w e. RR* /\ D e. RR* /\ B e. RR* ) -> ( ( w <_ D /\ D <_ B ) -> w <_ B ) )
7 4 4 5 6 ixxss12
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D <_ B ) ) -> ( C [,] D ) C_ ( A [,] B ) )
8 3 7 sylan
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ C /\ D <_ B ) ) -> ( C [,] D ) C_ ( A [,] B ) )