Theorem eliooxr

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

	Ref	Expression
Assertion	eliooxr	⊢ ( 𝐴 ∈ ( 𝐵 (,) 𝐶 ) → ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) )

Proof

Step	Hyp	Ref	Expression
1		ne0i	⊢ ( 𝐴 ∈ ( 𝐵 (,) 𝐶 ) → ( 𝐵 (,) 𝐶 ) ≠ ∅ )
2		ndmioo	⊢ ( ¬ ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐵 (,) 𝐶 ) = ∅ )
3	2	necon1ai	⊢ ( ( 𝐵 (,) 𝐶 ) ≠ ∅ → ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) )
4	1 3	syl	⊢ ( 𝐴 ∈ ( 𝐵 (,) 𝐶 ) → ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) )