Metamath Proof Explorer

Theorem eliooxr

Description: A nonempty open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008)

		Ref	Expression
	Assertion	eliooxr	$⊢ A \in (B, C) \to (B \in ℝ^{} \land C \in ℝ^{})$

Step	Hyp	Ref	Expression
1		ne0i	$⊢ A \in (B, C) \to (B, C) \neq \emptyset$
2		ndmioo	$⊢ \neg (B \in ℝ^{} \land C \in ℝ^{}) \to (B, C) = \emptyset$
3	2	necon1ai	$⊢ (B, C) \neq \emptyset \to (B \in ℝ^{} \land C \in ℝ^{})$
4	1 3	syl	$⊢ A \in (B, C) \to (B \in ℝ^{} \land C \in ℝ^{})$