Metamath Proof Explorer


Theorem mptmpoopabbrdOLD

Description: Obsolete version of mptmpoopabbrd as of 13-Dec-2024. (Contributed by Alexander van Vekens, 8-Nov-2017) (Revised by AV, 15-Jan-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses mptmpoopabbrdOLD.g φ G W
mptmpoopabbrdOLD.x φ X A G
mptmpoopabbrdOLD.y φ Y B G
mptmpoopabbrdOLD.v φ f h | ψ V
mptmpoopabbrdOLD.r φ f D G h ψ
mptmpoopabbrdOLD.1 a = X b = Y τ θ
mptmpoopabbrdOLD.2 g = G χ τ
mptmpoopabbrdOLD.m M = g V a A g , b B g f h | χ f D g h
Assertion mptmpoopabbrdOLD φ X M G Y = f h | θ f D G h

Proof

Step Hyp Ref Expression
1 mptmpoopabbrdOLD.g φ G W
2 mptmpoopabbrdOLD.x φ X A G
3 mptmpoopabbrdOLD.y φ Y B G
4 mptmpoopabbrdOLD.v φ f h | ψ V
5 mptmpoopabbrdOLD.r φ f D G h ψ
6 mptmpoopabbrdOLD.1 a = X b = Y τ θ
7 mptmpoopabbrdOLD.2 g = G χ τ
8 mptmpoopabbrdOLD.m M = g V a A g , b B g f h | χ f D g h
9 fveq2 g = G A g = A G
10 fveq2 g = G B g = B G
11 fveq2 g = G D g = D G
12 11 breqd g = G f D g h f D G h
13 7 12 anbi12d g = G χ f D g h τ f D G h
14 13 opabbidv g = G f h | χ f D g h = f h | τ f D G h
15 9 10 14 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
16 elex G W G V
17 16 adantr G W G W G V
18 fvex A G V
19 fvex B G V
20 18 19 pm3.2i A G V B G V
21 mpoexga A G V B G V a A G , b B G f h | τ f D G h V
22 20 21 mp1i G W G W a A G , b B G f h | τ f D G h V
23 8 15 17 22 fvmptd3 G W G W M G = a A G , b B G f h | τ f D G h
24 1 1 23 syl2anc φ M G = a A G , b B G f h | τ f D G h
25 24 oveqd φ X M G Y = X a A G , b B G f h | τ f D G h Y
26 ancom θ f D G h f D G h θ
27 26 opabbii f h | θ f D G h = f h | f D G h θ
28 5 4 opabresex2d φ f h | f D G h θ V
29 27 28 eqeltrid φ f h | θ f D G h V
30 6 anbi1d a = X b = Y τ f D G h θ f D G h
31 30 opabbidv a = X b = Y f h | τ f D G h = f h | θ f D G h
32 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
33 31 32 ovmpoga X A G Y B G f h | θ f D G h V X a A G , b B G f h | τ f D G h Y = f h | θ f D G h
34 2 3 29 33 syl3anc φ X a A G , b B G f h | τ f D G h Y = f h | θ f D G h
35 25 34 eqtrd φ X M G Y = f h | θ f D G h