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) Add disjoint variable condition on D , f , h to remove hypotheses. (Revised by SN, 13-Dec-2024)

	Ref	Expression
Hypotheses	mptmpoopabbrd.g	$⊢ φ \to G \in W$
	mptmpoopabbrd.x	$⊢ φ \to X \in A (G)$
	mptmpoopabbrd.y	$⊢ φ \to Y \in B (G)$
	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.1	$⊢ (a = X \land b = Y) \to (τ \leftrightarrow θ)$
5		mptmpoopabbrd.2	$⊢ g = G \to (χ \leftrightarrow τ)$
6		mptmpoopabbrd.m	$⊢ M = (g \in V ⟼ (a \in A (g), b \in B (g) ⟼ \{⟨f, h⟩ \| (χ \land f D (g) h)\}))$
7		fveq2	$⊢ g = G \to A (g) = A (G)$
8		fveq2	$⊢ g = G \to B (g) = B (G)$
9		fveq2	$⊢ g = G \to D (g) = D (G)$
10	9	breqd	$⊢ g = G \to (f D (g) h \leftrightarrow f D (G) h)$
11	5 10	anbi12d	$⊢ g = G \to ((χ \land f D (g) h) \leftrightarrow (τ \land f D (G) h))$
12	11	opabbidv	$⊢ g = G \to \{⟨f, h⟩ \| (χ \land f D (g) h)\} = \{⟨f, h⟩ \| (τ \land f D (G) h)\}$
13	7 8 12	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)\})$
14	1	elexd	$⊢ φ \to G \in V$
15		fvex	$⊢ A (G) \in V$
16		fvex	$⊢ B (G) \in V$
17	15 16	mpoex	$⊢ (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\}) \in V$
18	17	a1i	$⊢ φ \to (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\}) \in V$
19	6 13 14 18	fvmptd3	$⊢ φ \to M (G) = (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\})$
20	19	oveqd	$⊢ φ \to X M (G) Y = X (a \in A (G), b \in B (G) ⟼ \{⟨f, h⟩ \| (τ \land f D (G) h)\}) Y$
21	4	anbi1d	$⊢ (a = X \land b = Y) \to ((τ \land f D (G) h) \leftrightarrow (θ \land f D (G) h))$
22	21	opabbidv	$⊢ (a = X \land b = Y) \to \{⟨f, h⟩ \| (τ \land f D (G) h)\} = \{⟨f, h⟩ \| (θ \land f D (G) h)\}$
23		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)\})$
24		ancom	$⊢ (θ \land f D (G) h) \leftrightarrow (f D (G) h \land θ)$
25	24	opabbii	$⊢ \{⟨f, h⟩ \| (θ \land f D (G) h)\} = \{⟨f, h⟩ \| (f D (G) h \land θ)\}$
26		opabresex2	$⊢ \{⟨f, h⟩ \| (f D (G) h \land θ)\} \in V$
27	25 26	eqeltri	$⊢ \{⟨f, h⟩ \| (θ \land f D (G) h)\} \in V$
28	22 23 27	ovmpoa	$⊢ (X \in A (G) \land Y \in B (G)) \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)\}$
29	2 3 28	syl2anc	$⊢ φ \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)\}$
30	20 29	eqtrd	$⊢ φ \to X M (G) Y = \{⟨f, h⟩ \| (θ \land f D (G) h)\}$

Metamath Proof Explorer

Theorem mptmpoopabbrd

Proof