Metamath Proof Explorer


Theorem mptmpoopabovd

Description: The operation value of a function value of a collection of ordered pairs of related elements. (Contributed by Alexander van der 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
mptmpoopabovd.m M = g V a A g , b B g f h | f a C g b h f D g h
Assertion mptmpoopabovd φ X M G Y = f h | f X C G Y 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 mptmpoopabovd.m M = g V a A g , b B g f h | f a C g b h f D g h
5 oveq12 a = X b = Y a C G b = X C G Y
6 5 breqd a = X b = Y f a C G b h f X C G Y h
7 fveq2 g = G C g = C G
8 7 oveqd g = G a C g b = a C G b
9 8 breqd g = G f a C g b h f a C G b h
10 1 2 3 6 9 4 mptmpoopabbrd φ X M G Y = f h | f X C G Y h f D G h