ovg

Description: The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010)

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

Proof

Step	Hyp	Ref	Expression
1		ovg.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		ovg.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
3		ovg.3	$⊢ z = C \to (χ \leftrightarrow θ)$
4		ovg.4	$⊢ (τ \land (x \in R \land y \in S)) \to \exists! z φ$
5		ovg.5	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\}$
6		df-ov	$⊢ A F B = F (⟨A, B⟩)$
7	5	fveq1i	$⊢ F (⟨A, B⟩) = \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} (⟨A, B⟩)$
8	6 7	eqtri	$⊢ A F B = \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} (⟨A, B⟩)$
9	8	eqeq1i	$⊢ A F B = C \leftrightarrow \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} (⟨A, B⟩) = C$
10		eqeq2	$⊢ c = C \to (\{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} (⟨A, B⟩) = c \leftrightarrow \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} (⟨A, B⟩) = C)$
11		opeq2	$⊢ c = C \to ⟨⟨A, B⟩, c⟩ = ⟨⟨A, B⟩, C⟩$
12	11	eleq1d	$⊢ c = C \to (⟨⟨A, B⟩, c⟩ \in \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} \leftrightarrow ⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\})$
13	10 12	bibi12d	$⊢ c = C \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 φ)\}) \leftrightarrow (\{⟨⟨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 φ)\}))$
14	13	imbi2d	$⊢ c = C \to (((τ \land (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 φ)\})) \leftrightarrow ((τ \land (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 φ)\})))$
15	4	ex	$⊢ τ \to ((x \in R \land y \in S) \to \exists! z φ)$
16	15	alrimivv	$⊢ τ \to \forall x \forall y ((x \in R \land y \in S) \to \exists! z φ)$
17		fnoprabg	$⊢ \forall x \forall y ((x \in R \land y \in S) \to \exists! z φ) \to \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} Fn \{⟨x, y⟩ \| (x \in R \land y \in S)\}$
18	16 17	syl	$⊢ τ \to \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} Fn \{⟨x, y⟩ \| (x \in R \land y \in S)\}$
19		eleq1	$⊢ x = A \to (x \in R \leftrightarrow A \in R)$
20	19	anbi1d	$⊢ x = A \to ((x \in R \land y \in S) \leftrightarrow (A \in R \land y \in S))$
21		eleq1	$⊢ y = B \to (y \in S \leftrightarrow B \in S)$
22	21	anbi2d	$⊢ y = B \to ((A \in R \land y \in S) \leftrightarrow (A \in R \land B \in S))$
23	20 22	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))$
24	23	ibir	$⊢ (A \in R \land B \in S) \to ⟨A, B⟩ \in \{⟨x, y⟩ \| (x \in R \land y \in S)\}$
25		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 φ)\})$
26	18 24 25	syl2an	$⊢ (τ \land (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 φ)\})$
27	14 26	vtoclg	$⊢ C \in D \to ((τ \land (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 φ)\}))$
28	27	com12	$⊢ (τ \land (A \in R \land B \in S)) \to (C \in D \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 φ)\}))$
29	28	exp32	$⊢ τ \to (A \in R \to (B \in S \to (C \in D \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 φ)\}))))$
30	29	3imp2	$⊢ (τ \land (A \in R \land B \in S \land C \in D)) \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 φ)\})$
31	20 1	anbi12d	$⊢ x = A \to (((x \in R \land y \in S) \land φ) \leftrightarrow ((A \in R \land y \in S) \land ψ))$
32	22 2	anbi12d	$⊢ y = B \to (((A \in R \land y \in S) \land ψ) \leftrightarrow ((A \in R \land B \in S) \land χ))$
33	3	anbi2d	$⊢ z = C \to (((A \in R \land B \in S) \land χ) \leftrightarrow ((A \in R \land B \in S) \land θ))$
34	31 32 33	eloprabg	$⊢ (A \in R \land B \in S \land C \in D) \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 θ))$
35	34	adantl	$⊢ (τ \land (A \in R \land B \in S \land C \in D)) \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 θ))$
36	30 35	bitrd	$⊢ (τ \land (A \in R \land B \in S \land C \in D)) \to (\{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} (⟨A, B⟩) = C \leftrightarrow ((A \in R \land B \in S) \land θ))$
37	9 36	bitrid	$⊢ (τ \land (A \in R \land B \in S \land C \in D)) \to (A F B = C \leftrightarrow ((A \in R \land B \in S) \land θ))$
38		biidd	$⊢ (A \in R \land B \in S) \to (((A \in R \land B \in S) \land θ) \leftrightarrow ((A \in R \land B \in S) \land θ))$
39	38	bianabs	$⊢ (A \in R \land B \in S) \to (((A \in R \land B \in S) \land θ) \leftrightarrow θ)$
40	39	3adant3	$⊢ (A \in R \land B \in S \land C \in D) \to (((A \in R \land B \in S) \land θ) \leftrightarrow θ)$
41	40	adantl	$⊢ (τ \land (A \in R \land B \in S \land C \in D)) \to (((A \in R \land B \in S) \land θ) \leftrightarrow θ)$
42	37 41	bitrd	$⊢ (τ \land (A \in R \land B \in S \land C \in D)) \to (A F B = C \leftrightarrow θ)$

Metamath Proof Explorer

Theorem ovg

Proof