Theorem elioore

Description: A member of an open interval of reals is a real. (Contributed by NM, 17-Aug-2008) (Revised by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Assertion	elioore	⊢ ( 𝐴 ∈ ( 𝐵 (,) 𝐶 ) → 𝐴 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		elioo3g	⊢ ( 𝐴 ∈ ( 𝐵 (,) 𝐶 ) ↔ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) ∧ ( 𝐵 < 𝐴 ∧ 𝐴 < 𝐶 ) ) )
2		3ancomb	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) ↔ ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) )
3		xrre2	⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐵 < 𝐴 ∧ 𝐴 < 𝐶 ) ) → 𝐴 ∈ ℝ )
4	2 3	sylanb	⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) ∧ ( 𝐵 < 𝐴 ∧ 𝐴 < 𝐶 ) ) → 𝐴 ∈ ℝ )
5	1 4	sylbi	⊢ ( 𝐴 ∈ ( 𝐵 (,) 𝐶 ) → 𝐴 ∈ ℝ )