Metamath Proof Explorer

Theorem ioossioo

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

Ref Expression
Assertion ioossioo 
|- ( ( ( 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 xrlelttr 
 |-  ( ( A e. RR* /\ C e. RR* /\ w e. RR* ) -> ( ( A <_ C /\ C < w ) -> A < w ) )
3 xrltletr 
 |-  ( ( w e. RR* /\ D e. RR* /\ B e. RR* ) -> ( ( w < D /\ D <_ B ) -> w < B ) )
4 1 1 2 3 ixxss12 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D <_ B ) ) -> ( C (,) D ) C_ ( A (,) B ) )