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; avoid ax-rep . (Revised by SN, 7-Apr-2025)

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 fvex D G V
18 17 pwex 𝒫 D G V
19 simpr τ f D G h f D G h
20 19 ssopab2i f h | τ f D G h f h | f D G h
21 opabss f h | f D G h D G
22 20 21 sstri f h | τ f D G h D G
23 17 22 elpwi2 f h | τ f D G h 𝒫 D G
24 23 rgen2w a A G b B G f h | τ f D G h 𝒫 D G
25 15 16 18 24 mpoexw a A G , b B G f h | τ f D G h V
26 25 a1i φ a A G , b B G f h | τ f D G h V
27 6 13 14 26 fvmptd3 φ M G = a A G , b B G f h | τ f D G h
28 27 oveqd φ X M G Y = X a A G , b B G f h | τ f D G h Y
29 4 anbi1d a = X b = Y τ f D G h θ f D G h
30 29 opabbidv a = X b = Y f h | τ f D G h = f h | θ f D G h
31 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
32 ancom θ f D G h f D G h θ
33 32 opabbii f h | θ f D G h = f h | f D G h θ
34 opabresex2 f h | f D G h θ V
35 33 34 eqeltri f h | θ f D G h V
36 30 31 35 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
37 2 3 36 syl2anc φ X a A G , b B G f h | τ f D G h Y = f h | θ f D G h
38 28 37 eqtrd φ X M G Y = f h | θ f D G h