mptmpoopabbrd

Description: The operation value of a function value of a collection of ordered pairs of elements related in two ways. (Contributed by Alexander van Vekens, 8-Nov-2017) (Revised by AV, 15-Jan-2021)

	Ref	Expression
Hypotheses	mptmpoopabbrd.g	$⊢ φ \to G \in W$
	mptmpoopabbrd.x	$⊢ φ \to X \in A (G)$
	mptmpoopabbrd.y	$⊢ φ \to Y \in B (G)$
	mptmpoopabbrd.v	$⊢ φ \to \{⟨f, h⟩ \| ψ\} \in V$
	mptmpoopabbrd.r	$⊢ (φ \land f D (G) h) \to ψ$
	mptmpoopabbrd.1	$⊢ (a = X \land b = Y) \to (τ \leftrightarrow θ)$
	mptmpoopabbrd.2	$⊢ g = G \to (χ \leftrightarrow τ)$
	mptmpoopabbrd.m	$⊢ M = (g \in V ⟼ (a \in A (g), b \in B (g) ⟼ \{⟨f, h⟩ \| (χ \land f D (g) h)\}))$
Assertion	mptmpoopabbrd	$⊢ φ \to X M (G) Y = \{⟨f, h⟩ \| (θ \land f D (G) h)\}$

Proof

Step	Hyp	Ref	Expression
1		mptmpoopabbrd.g	$⊢ φ \to G \in W$
2		mptmpoopabbrd.x	$⊢ φ \to X \in A (G)$
3		mptmpoopabbrd.y	$⊢ φ \to Y \in B (G)$
4		mptmpoopabbrd.v	$⊢ φ \to \{⟨f, h⟩ \| ψ\} \in V$
5		mptmpoopabbrd.r	$⊢ (φ \land f D (G) h) \to ψ$
6		mptmpoopabbrd.1	$⊢ (a = X \land b = Y) \to (τ \leftrightarrow θ)$
7		mptmpoopabbrd.2	$⊢ g = G \to (χ \leftrightarrow τ)$
8		mptmpoopabbrd.m	$⊢ M = (g \in V ⟼ (a \in A (g), b \in B (g) ⟼ \{⟨f, h⟩ \| (χ \land f D (g) h)\}))$
9		fveq2	$⊢ g = G \to A (g) = A (G)$
10		fveq2	$⊢ g = G \to B (g) = B (G)$
11		fveq2	$⊢ g = G \to D (g) = D (G)$
12	11	breqd	$⊢ g = G \to (f D (g) h \leftrightarrow f D (G) h)$
13	7 12	anbi12d	$⊢ g = G \to ((χ \land f D (g) h) \leftrightarrow (τ \land f D (G) h))$
14	13	opabbidv	$⊢ g = G \to \{⟨f, h⟩ \| (χ \land f D (g) h)\} = \{⟨f, h⟩ \| (τ \land f D (G) h)\}$
15	9 10 14	mpoeq123dv	$⊢ g = G \to (a \in A (g), b \in B (g) ⟼ \{⟨f, h⟩ \| (χ \land f D (g) h)\}) = (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\})$
16		elex	$⊢ G \in W \to G \in V$
17	16	adantr	$⊢ (G \in W \land G \in W) \to G \in V$
18		fvex	$⊢ A (G) \in V$
19		fvex	$⊢ B (G) \in V$
20	18 19	pm3.2i	$⊢ (A (G) \in V \land B (G) \in V)$
21		mpoexga	$⊢ (A (G) \in V \land B (G) \in V) \to (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\}) \in V$
22	20 21	mp1i	$⊢ (G \in W \land G \in W) \to (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\}) \in V$
23	8 15 17 22	fvmptd3	$⊢ (G \in W \land G \in W) \to M (G) = (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\})$
24	1 1 23	syl2anc	$⊢ φ \to M (G) = (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\})$
25	24	oveqd	$⊢ φ \to X M (G) Y = X (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\}) Y$
26		ancom	$⊢ (θ \land f D (G) h) \leftrightarrow (f D (G) h \land θ)$
27	26	opabbii	$⊢ \{⟨f, h⟩ \| (θ \land f D (G) h)\} = \{⟨f, h⟩ \| (f D (G) h \land θ)\}$
28	5 4	opabresex2d	$⊢ φ \to \{⟨f, h⟩ \| (f D (G) h \land θ)\} \in V$
29	27 28	eqeltrid	$⊢ φ \to \{⟨f, h⟩ \| (θ \land f D (G) h)\} \in V$
30	6	anbi1d	$⊢ (a = X \land b = Y) \to ((τ \land f D (G) h) \leftrightarrow (θ \land f D (G) h))$
31	30	opabbidv	$⊢ (a = X \land b = Y) \to \{⟨f, h⟩ \| (τ \land f D (G) h)\} = \{⟨f, h⟩ \| (θ \land f D (G) h)\}$
32		eqid	$⊢ (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\}) = (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\})$
33	31 32	ovmpoga	$⊢ (X \in A (G) \land Y \in B (G) \land \{⟨f, h⟩ \| (θ \land f D (G) h)\} \in V) \to X (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\}) Y = \{⟨f, h⟩ \| (θ \land f D (G) h)\}$
34	2 3 29 33	syl3anc	$⊢ φ \to X (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\}) Y = \{⟨f, h⟩ \| (θ \land f D (G) h)\}$
35	25 34	eqtrd	$⊢ φ \to X M (G) Y = \{⟨f, h⟩ \| (θ \land f D (G) h)\}$

Metamath Proof Explorer

Theorem mptmpoopabbrd

Proof