elixx1

Description: Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013)

		Ref	Expression
	Hypothesis	ixx.1	$⊢ O = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x R z \land z S y)\})$
	Assertion	elixx1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (C \in (A O B) \leftrightarrow (C \in ℝ^{*} \land A R C \land C S B))$

Step	Hyp	Ref	Expression
1		ixx.1	$⊢ O = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x R z \land z S y)\})$
2	1	ixxval	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A O B = \{z \in ℝ^{*} \| (A R z \land z S B)\}$
3	2	eleq2d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (C \in (A O B) \leftrightarrow C \in \{z \in ℝ^{*} \| (A R z \land z S B)\})$
4		breq2	$⊢ z = C \to (A R z \leftrightarrow A R C)$
5		breq1	$⊢ z = C \to (z S B \leftrightarrow C S B)$
6	4 5	anbi12d	$⊢ z = C \to ((A R z \land z S B) \leftrightarrow (A R C \land C S B))$
7	6	elrab	$⊢ C \in \{z \in ℝ^{} \| (A R z \land z S B)\} \leftrightarrow (C \in ℝ^{} \land (A R C \land C S B))$
8		3anass	$⊢ (C \in ℝ^{} \land A R C \land C S B) \leftrightarrow (C \in ℝ^{} \land (A R C \land C S B))$
9	7 8	bitr4i	$⊢ C \in \{z \in ℝ^{} \| (A R z \land z S B)\} \leftrightarrow (C \in ℝ^{} \land A R C \land C S B)$
10	3 9	bitrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (C \in (A O B) \leftrightarrow (C \in ℝ^{*} \land A R C \land C S B))$

Metamath Proof Explorer