ixxval

Description: Value of the interval function. (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	ixxval	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A O B = \{z \in ℝ^{*} \| (A R z \land z S B)\}$

Step	Hyp	Ref	Expression
1		ixx.1	$⊢ O = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x R z \land z S y)\})$
2		breq1	$⊢ x = A \to (x R z \leftrightarrow A R z)$
3	2	anbi1d	$⊢ x = A \to ((x R z \land z S y) \leftrightarrow (A R z \land z S y))$
4	3	rabbidv	$⊢ x = A \to \{z \in ℝ^{} \| (x R z \land z S y)\} = \{z \in ℝ^{} \| (A R z \land z S y)\}$
5		breq2	$⊢ y = B \to (z S y \leftrightarrow z S B)$
6	5	anbi2d	$⊢ y = B \to ((A R z \land z S y) \leftrightarrow (A R z \land z S B))$
7	6	rabbidv	$⊢ y = B \to \{z \in ℝ^{} \| (A R z \land z S y)\} = \{z \in ℝ^{} \| (A R z \land z S B)\}$
8		xrex	$⊢ ℝ^{*} \in V$
9	8	rabex	$⊢ \{z \in ℝ^{*} \| (A R z \land z S B)\} \in V$
10	4 7 1 9	ovmpo	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A O B = \{z \in ℝ^{*} \| (A R z \land z S B)\}$

Metamath Proof Explorer