eliooord

Description: Ordering implied by a member of an open interval of reals. (Contributed by NM, 17-Aug-2008) (Revised by Mario Carneiro, 9-May-2014)

		Ref	Expression
	Assertion	eliooord	$⊢ A \in (B, C) \to (B < A \land A < C)$

Step	Hyp	Ref	Expression
1		eliooxr	$⊢ A \in (B, C) \to (B \in ℝ^{} \land C \in ℝ^{})$
2		elioo2	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to (A \in (B, C) \leftrightarrow (A \in ℝ \land B < A \land A < C))$
3	1 2	syl	$⊢ A \in (B, C) \to (A \in (B, C) \leftrightarrow (A \in ℝ \land B < A \land A < C))$
4	3	ibi	$⊢ A \in (B, C) \to (A \in ℝ \land B < A \land A < C)$
5		3simpc	$⊢ (A \in ℝ \land B < A \land A < C) \to (B < A \land A < C)$
6	4 5	syl	$⊢ A \in (B, C) \to (B < A \land A < C)$

Metamath Proof Explorer