Metamath Proof Explorer


Theorem 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 φ G W
mptmpoopabbrd.x φ X A G
mptmpoopabbrd.y φ Y B G
mptmpoopabbrd.1 a = X b = Y τ θ
mptmpoopabbrd.2 g = G χ τ
mptmpoopabbrd.m M = g V a A g , b B g f h | χ f D g h
Assertion mptmpoopabbrd φ X M G Y = f h | θ f D G h

Proof

Step Hyp Ref Expression
1 mptmpoopabbrd.g φ G W
2 mptmpoopabbrd.x φ X A G
3 mptmpoopabbrd.y φ Y B G
4 mptmpoopabbrd.1 a = X b = Y τ θ
5 mptmpoopabbrd.2 g = G χ τ
6 mptmpoopabbrd.m M = g V a A g , b B g f h | χ f D g h
7 fveq2 g = G A g = A G
8 fveq2 g = G B g = B G
9 fveq2 g = G D g = D G
10 9 breqd g = G f D g h f D G h
11 5 10 anbi12d g = G χ f D g h τ f D G h
12 11 opabbidv g = G f h | χ f D g h = f h | τ f D G h
13 7 8 12 mpoeq123dv g = G a A g , b B g f h | χ f D g h = a A G , b B G f h | τ f D G h
14 1 elexd φ G V
15 fvex A G V
16 fvex B G V
17 15 16 mpoex a A G , b B G f h | τ f D G h V
18 17 a1i φ a A G , b B G f h | τ f D G h V
19 6 13 14 18 fvmptd3 φ M G = a A G , b B G f h | τ f D G h
20 19 oveqd φ X M G Y = X a A G , b B G f h | τ f D G h Y
21 4 anbi1d a = X b = Y τ f D G h θ f D G h
22 21 opabbidv a = X b = Y f h | τ f D G h = f h | θ f D G h
23 eqid a A G , b B G f h | τ f D G h = a A G , b B G f h | τ f D G h
24 ancom θ f D G h f D G h θ
25 24 opabbii f h | θ f D G h = f h | f D G h θ
26 opabresex2 f h | f D G h θ V
27 25 26 eqeltri f h | θ f D G h V
28 22 23 27 ovmpoa X A G Y B G X a A G , b B G f h | τ f D G h Y = f h | θ f D G h
29 2 3 28 syl2anc φ X a A G , b B G f h | τ f D G h Y = f h | θ f D G h
30 20 29 eqtrd φ X M G Y = f h | θ f D G h