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