ov

Description: The value of an operation class abstraction. (Contributed by NM, 16-May-1995) (Revised by David Abernethy, 19-Jun-2012)

	Ref	Expression
Hypotheses	ov.1	$⊢ C \in V$
	ov.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
	ov.3	$⊢ y = B \to (ψ \leftrightarrow χ)$
	ov.4	$⊢ z = C \to (χ \leftrightarrow θ)$
	ov.5	$⊢ (x \in R \land y \in S) \to \exists! z φ$
	ov.6	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\}$
Assertion	ov	$⊢ (A \in R \land B \in S) \to (A F B = C \leftrightarrow θ)$

Proof

Step	Hyp	Ref	Expression
1		ov.1	$⊢ C \in V$
2		ov.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
3		ov.3	$⊢ y = B \to (ψ \leftrightarrow χ)$
4		ov.4	$⊢ z = C \to (χ \leftrightarrow θ)$
5		ov.5	$⊢ (x \in R \land y \in S) \to \exists! z φ$
6		ov.6	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\}$
7		df-ov	$⊢ A F B = F (⟨A, B⟩)$
8	6	fveq1i	$⊢ F (⟨A, B⟩) = \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} (⟨A, B⟩)$
9	7 8	eqtri	$⊢ A F B = \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} (⟨A, B⟩)$
10	9	eqeq1i	$⊢ A F B = C \leftrightarrow \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} (⟨A, B⟩) = C$
11	5	fnoprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} Fn \{⟨x, y⟩ \| (x \in R \land y \in S)\}$
12		eleq1	$⊢ x = A \to (x \in R \leftrightarrow A \in R)$
13	12	anbi1d	$⊢ x = A \to ((x \in R \land y \in S) \leftrightarrow (A \in R \land y \in S))$
14		eleq1	$⊢ y = B \to (y \in S \leftrightarrow B \in S)$
15	14	anbi2d	$⊢ y = B \to ((A \in R \land y \in S) \leftrightarrow (A \in R \land B \in S))$
16	13 15	opelopabg	$⊢ (A \in R \land B \in S) \to (⟨A, B⟩ \in \{⟨x, y⟩ \| (x \in R \land y \in S)\} \leftrightarrow (A \in R \land B \in S))$
17	16	ibir	$⊢ (A \in R \land B \in S) \to ⟨A, B⟩ \in \{⟨x, y⟩ \| (x \in R \land y \in S)\}$
18		fnopfvb	$⊢ (\{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} Fn \{⟨x, y⟩ \| (x \in R \land y \in S)\} \land ⟨A, B⟩ \in \{⟨x, y⟩ \| (x \in R \land y \in S)\}) \to (\{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} (⟨A, B⟩) = C \leftrightarrow ⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\})$
19	11 17 18	sylancr	$⊢ (A \in R \land B \in S) \to (\{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} (⟨A, B⟩) = C \leftrightarrow ⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\})$
20	13 2	anbi12d	$⊢ x = A \to (((x \in R \land y \in S) \land φ) \leftrightarrow ((A \in R \land y \in S) \land ψ))$
21	15 3	anbi12d	$⊢ y = B \to (((A \in R \land y \in S) \land ψ) \leftrightarrow ((A \in R \land B \in S) \land χ))$
22	4	anbi2d	$⊢ z = C \to (((A \in R \land B \in S) \land χ) \leftrightarrow ((A \in R \land B \in S) \land θ))$
23	20 21 22	eloprabg	$⊢ (A \in R \land B \in S \land C \in V) \to (⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} \leftrightarrow ((A \in R \land B \in S) \land θ))$
24	1 23	mp3an3	$⊢ (A \in R \land B \in S) \to (⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} \leftrightarrow ((A \in R \land B \in S) \land θ))$
25	19 24	bitrd	$⊢ (A \in R \land B \in S) \to (\{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} (⟨A, B⟩) = C \leftrightarrow ((A \in R \land B \in S) \land θ))$
26	10 25	syl5bb	$⊢ (A \in R \land B \in S) \to (A F B = C \leftrightarrow ((A \in R \land B \in S) \land θ))$
27	26	bianabs	$⊢ (A \in R \land B \in S) \to (A F B = C \leftrightarrow θ)$

Metamath Proof Explorer

Theorem ov

Proof