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 ( 𝜑𝐺𝑊 )
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 fvex ( 𝐷𝐺 ) ∈ V
18 17 pwex 𝒫 ( 𝐷𝐺 ) ∈ V
19 simpr ( ( 𝜏𝑓 ( 𝐷𝐺 ) ) → 𝑓 ( 𝐷𝐺 ) )
20 19 ssopab2i { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ⊆ { ⟨ 𝑓 , ⟩ ∣ 𝑓 ( 𝐷𝐺 ) }
21 opabss { ⟨ 𝑓 , ⟩ ∣ 𝑓 ( 𝐷𝐺 ) } ⊆ ( 𝐷𝐺 )
22 20 21 sstri { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ⊆ ( 𝐷𝐺 )
23 17 22 elpwi2 { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ∈ 𝒫 ( 𝐷𝐺 )
24 23 rgen2w 𝑎 ∈ ( 𝐴𝐺 ) ∀ 𝑏 ∈ ( 𝐵𝐺 ) { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ∈ 𝒫 ( 𝐷𝐺 )
25 15 16 18 24 mpoexw ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) ∈ V
26 25 a1i ( 𝜑 → ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) ∈ V )
27 6 13 14 26 fvmptd3 ( 𝜑 → ( 𝑀𝐺 ) = ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) )
28 27 oveqd ( 𝜑 → ( 𝑋 ( 𝑀𝐺 ) 𝑌 ) = ( 𝑋 ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) 𝑌 ) )
29 4 anbi1d ( ( 𝑎 = 𝑋𝑏 = 𝑌 ) → ( ( 𝜏𝑓 ( 𝐷𝐺 ) ) ↔ ( 𝜃𝑓 ( 𝐷𝐺 ) ) ) )
30 29 opabbidv ( ( 𝑎 = 𝑋𝑏 = 𝑌 ) → { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } = { ⟨ 𝑓 , ⟩ ∣ ( 𝜃𝑓 ( 𝐷𝐺 ) ) } )
31 eqid ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) = ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } )
32 ancom ( ( 𝜃𝑓 ( 𝐷𝐺 ) ) ↔ ( 𝑓 ( 𝐷𝐺 ) 𝜃 ) )
33 32 opabbii { ⟨ 𝑓 , ⟩ ∣ ( 𝜃𝑓 ( 𝐷𝐺 ) ) } = { ⟨ 𝑓 , ⟩ ∣ ( 𝑓 ( 𝐷𝐺 ) 𝜃 ) }
34 opabresex2 { ⟨ 𝑓 , ⟩ ∣ ( 𝑓 ( 𝐷𝐺 ) 𝜃 ) } ∈ V
35 33 34 eqeltri { ⟨ 𝑓 , ⟩ ∣ ( 𝜃𝑓 ( 𝐷𝐺 ) ) } ∈ V
36 30 31 35 ovmpoa ( ( 𝑋 ∈ ( 𝐴𝐺 ) ∧ 𝑌 ∈ ( 𝐵𝐺 ) ) → ( 𝑋 ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) 𝑌 ) = { ⟨ 𝑓 , ⟩ ∣ ( 𝜃𝑓 ( 𝐷𝐺 ) ) } )
37 2 3 36 syl2anc ( 𝜑 → ( 𝑋 ( 𝑎 ∈ ( 𝐴𝐺 ) , 𝑏 ∈ ( 𝐵𝐺 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝜏𝑓 ( 𝐷𝐺 ) ) } ) 𝑌 ) = { ⟨ 𝑓 , ⟩ ∣ ( 𝜃𝑓 ( 𝐷𝐺 ) ) } )
38 28 37 eqtrd ( 𝜑 → ( 𝑋 ( 𝑀𝐺 ) 𝑌 ) = { ⟨ 𝑓 , ⟩ ∣ ( 𝜃𝑓 ( 𝐷𝐺 ) ) } )