This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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