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

Metamath Proof Explorer

Theorem iccssioo2

Description: Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( C e. ( A (,) B ) -> ( A (,) B ) =/= (/) )
2 1 adantr 
 |-  ( ( C e. ( A (,) B ) /\ D e. ( A (,) B ) ) -> ( A (,) B ) =/= (/) )
3 ndmioo 
 |-  ( -. ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = (/) )
4 3 necon1ai 
 |-  ( ( A (,) B ) =/= (/) -> ( A e. RR* /\ B e. RR* ) )
5 2 4 syl 
 |-  ( ( C e. ( A (,) B ) /\ D e. ( A (,) B ) ) -> ( A e. RR* /\ B e. RR* ) )
6 eliooord 
 |-  ( C e. ( A (,) B ) -> ( A < C /\ C < B ) )
7 6 adantr 
 |-  ( ( C e. ( A (,) B ) /\ D e. ( A (,) B ) ) -> ( A < C /\ C < B ) )
8 7 simpld 
 |-  ( ( C e. ( A (,) B ) /\ D e. ( A (,) B ) ) -> A < C )
9 eliooord 
 |-  ( D e. ( A (,) B ) -> ( A < D /\ D < B ) )
10 9 adantl 
 |-  ( ( C e. ( A (,) B ) /\ D e. ( A (,) B ) ) -> ( A < D /\ D < B ) )
11 10 simprd 
 |-  ( ( C e. ( A (,) B ) /\ D e. ( A (,) B ) ) -> D < B )
12 iccssioo 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( A < C /\ D < B ) ) -> ( C [,] D ) C_ ( A (,) B ) )
13 5 8 11 12 syl12anc 
 |-  ( ( C e. ( A (,) B ) /\ D e. ( A (,) B ) ) -> ( C [,] D ) C_ ( A (,) B ) )