elioo4g

Description: Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007) (Revised by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	elioo4g	$⊢ C \in (A, B) \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ) \land (A < C \land C < B))$

Step	Hyp	Ref	Expression
1		eliooxr	$⊢ C \in (A, B) \to (A \in ℝ^{} \land B \in ℝ^{})$
2		elioore	$⊢ C \in (A, B) \to C \in ℝ$
3	1 2	jca	$⊢ C \in (A, B) \to ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ)$
4		df-3an	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ) \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ)$
5	3 4	sylibr	$⊢ C \in (A, B) \to (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ)$
6		eliooord	$⊢ C \in (A, B) \to (A < C \land C < B)$
7	5 6	jca	$⊢ C \in (A, B) \to ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ) \land (A < C \land C < B))$
8		rexr	$⊢ C \in ℝ \to C \in ℝ^{*}$
9	8	3anim3i	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ) \to (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*})$
10	9	anim1i	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ) \land (A < C \land C < B)) \to ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < C \land C < B))$
11		elioo3g	$⊢ C \in (A, B) \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < C \land C < B))$
12	10 11	sylibr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ) \land (A < C \land C < B)) \to C \in (A, B)$
13	7 12	impbii	$⊢ C \in (A, B) \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ) \land (A < C \land C < B))$

Metamath Proof Explorer