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 ( 𝜑𝐺𝑊 )
mptmpoopabbrd.x ( 𝜑𝑋 ∈ ( 𝐴𝐺 ) )
mptmpoopabbrd.y ( 𝜑𝑌 ∈ ( 𝐵𝐺 ) )
mptmpoopabbrd.1 ( ( 𝑎 = 𝑋𝑏 = 𝑌 ) → ( 𝜏𝜃 ) )
mptmpoopabbrd.2 ( 𝑔 = 𝐺 → ( 𝜒𝜏 ) )
mptmpoopabbrd.m 𝑀 = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( 𝐴𝑔 ) , 𝑏 ∈ ( 𝐵𝑔 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜒𝑓 ( 𝐷𝑔 ) ) } ) )
Assertion mptmpoopabbrd ( 𝜑 → ( 𝑋 ( 𝑀𝐺 ) 𝑌 ) = { ⟨ 𝑓 , ⟩ ∣ ( 𝜃𝑓 ( 𝐷𝐺 ) ) } )

Proof

Step Hyp Ref Expression
1 mptmpoopabbrd.g ( 𝜑𝐺𝑊 )
2 mptmpoopabbrd.x ( 𝜑𝑋 ∈ ( 𝐴𝐺 ) )
3 mptmpoopabbrd.y ( 𝜑𝑌 ∈ ( 𝐵𝐺 ) )
4 mptmpoopabbrd.1 ( ( 𝑎 = 𝑋𝑏 = 𝑌 ) → ( 𝜏𝜃 ) )
5 mptmpoopabbrd.2 ( 𝑔 = 𝐺 → ( 𝜒𝜏 ) )
6 mptmpoopabbrd.m 𝑀 = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( 𝐴𝑔 ) , 𝑏 ∈ ( 𝐵𝑔 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜒𝑓 ( 𝐷𝑔 ) ) } ) )
7 fveq2 ( 𝑔 = 𝐺 → ( 𝐴𝑔 ) = ( 𝐴𝐺 ) )
8 fveq2 ( 𝑔 = 𝐺 → ( 𝐵𝑔 ) = ( 𝐵𝐺 ) )
9 fveq2 ( 𝑔 = 𝐺 → ( 𝐷𝑔 ) = ( 𝐷𝐺 ) )
10 9 breqd ( 𝑔 = 𝐺 → ( 𝑓 ( 𝐷𝑔 ) 𝑓 ( 𝐷𝐺 ) ) )
11 5 10 anbi12d ( 𝑔 = 𝐺 → ( ( 𝜒𝑓 ( 𝐷𝑔 ) ) ↔ ( 𝜏𝑓 ( 𝐷𝐺 ) ) ) )
12 11 opabbidv ( 𝑔 = 𝐺 → { ⟨ 𝑓 , ⟩ ∣ ( 𝜒𝑓 ( 𝐷𝑔 ) ) } = { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } )
13 7 8 12 mpoeq123dv ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( 𝐴𝑔 ) , 𝑏 ∈ ( 𝐵𝑔 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜒𝑓 ( 𝐷𝑔 ) ) } ) = ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) )
14 1 elexd ( 𝜑𝐺 ∈ V )
15 fvex ( 𝐴𝐺 ) ∈ V
16 fvex ( 𝐵𝐺 ) ∈ V
17 15 16 mpoex ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) ∈ V
18 17 a1i ( 𝜑 → ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) ∈ V )
19 6 13 14 18 fvmptd3 ( 𝜑 → ( 𝑀𝐺 ) = ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) )
20 19 oveqd ( 𝜑 → ( 𝑋 ( 𝑀𝐺 ) 𝑌 ) = ( 𝑋 ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) 𝑌 ) )
21 4 anbi1d ( ( 𝑎 = 𝑋𝑏 = 𝑌 ) → ( ( 𝜏𝑓 ( 𝐷𝐺 ) ) ↔ ( 𝜃𝑓 ( 𝐷𝐺 ) ) ) )
22 21 opabbidv ( ( 𝑎 = 𝑋𝑏 = 𝑌 ) → { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } = { ⟨ 𝑓 , ⟩ ∣ ( 𝜃𝑓 ( 𝐷𝐺 ) ) } )
23 eqid ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) = ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } )
24 ancom ( ( 𝜃𝑓 ( 𝐷𝐺 ) ) ↔ ( 𝑓 ( 𝐷𝐺 ) 𝜃 ) )
25 24 opabbii { ⟨ 𝑓 , ⟩ ∣ ( 𝜃𝑓 ( 𝐷𝐺 ) ) } = { ⟨ 𝑓 , ⟩ ∣ ( 𝑓 ( 𝐷𝐺 ) 𝜃 ) }
26 opabresex2 { ⟨ 𝑓 , ⟩ ∣ ( 𝑓 ( 𝐷𝐺 ) 𝜃 ) } ∈ V
27 25 26 eqeltri { ⟨ 𝑓 , ⟩ ∣ ( 𝜃𝑓 ( 𝐷𝐺 ) ) } ∈ V
28 22 23 27 ovmpoa ( ( 𝑋 ∈ ( 𝐴𝐺 ) ∧ 𝑌 ∈ ( 𝐵𝐺 ) ) → ( 𝑋 ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) 𝑌 ) = { ⟨ 𝑓 , ⟩ ∣ ( 𝜃𝑓 ( 𝐷𝐺 ) ) } )
29 2 3 28 syl2anc ( 𝜑 → ( 𝑋 ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) 𝑌 ) = { ⟨ 𝑓 , ⟩ ∣ ( 𝜃𝑓 ( 𝐷𝐺 ) ) } )
30 20 29 eqtrd ( 𝜑 → ( 𝑋 ( 𝑀𝐺 ) 𝑌 ) = { ⟨ 𝑓 , ⟩ ∣ ( 𝜃𝑓 ( 𝐷𝐺 ) ) } )