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 \in (A, B) \land D \in (A, B)) \to [C, D] \subseteq (A, B)$

Step	Hyp	Ref	Expression
1		ne0i	$⊢ C \in (A, B) \to (A, B) \neq \emptyset$
2	1	adantr	$⊢ (C \in (A, B) \land D \in (A, B)) \to (A, B) \neq \emptyset$
3		ndmioo	$⊢ \neg (A \in ℝ^{} \land B \in ℝ^{}) \to (A, B) = \emptyset$
4	3	necon1ai	$⊢ (A, B) \neq \emptyset \to (A \in ℝ^{} \land B \in ℝ^{})$
5	2 4	syl	$⊢ (C \in (A, B) \land D \in (A, B)) \to (A \in ℝ^{} \land B \in ℝ^{})$
6		eliooord	$⊢ C \in (A, B) \to (A < C \land C < B)$
7	6	adantr	$⊢ (C \in (A, B) \land D \in (A, B)) \to (A < C \land C < B)$
8	7	simpld	$⊢ (C \in (A, B) \land D \in (A, B)) \to A < C$
9		eliooord	$⊢ D \in (A, B) \to (A < D \land D < B)$
10	9	adantl	$⊢ (C \in (A, B) \land D \in (A, B)) \to (A < D \land D < B)$
11	10	simprd	$⊢ (C \in (A, B) \land D \in (A, B)) \to D < B$
12		iccssioo	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < C \land D < B)) \to [C, D] \subseteq (A, B)$
13	5 8 11 12	syl12anc	$⊢ (C \in (A, B) \land D \in (A, B)) \to [C, D] \subseteq (A, B)$

Metamath Proof Explorer