Metamath Proof Explorer


Theorem mptmpoopabovdOLD

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

Ref Expression
Hypotheses mptmpoopabbrdOLD.g ( 𝜑𝐺𝑊 )
mptmpoopabbrdOLD.x ( 𝜑𝑋 ∈ ( 𝐴𝐺 ) )
mptmpoopabbrdOLD.y ( 𝜑𝑌 ∈ ( 𝐵𝐺 ) )
mptmpoopabbrdOLD.v ( 𝜑 → { ⟨ 𝑓 , ⟩ ∣ 𝜓 } ∈ 𝑉 )
mptmpoopabbrdOLD.r ( ( 𝜑𝑓 ( 𝐷𝐺 ) ) → 𝜓 )
mptmpoopabovdOLD.m 𝑀 = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( 𝐴𝑔 ) , 𝑏 ∈ ( 𝐵𝑔 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝑓 ( 𝑎 ( 𝐶𝑔 ) 𝑏 ) 𝑓 ( 𝐷𝑔 ) ) } ) )
Assertion mptmpoopabovdOLD ( 𝜑 → ( 𝑋 ( 𝑀𝐺 ) 𝑌 ) = { ⟨ 𝑓 , ⟩ ∣ ( 𝑓 ( 𝑋 ( 𝐶𝐺 ) 𝑌 ) 𝑓 ( 𝐷𝐺 ) ) } )

Proof

Step Hyp Ref Expression
1 mptmpoopabbrdOLD.g ( 𝜑𝐺𝑊 )
2 mptmpoopabbrdOLD.x ( 𝜑𝑋 ∈ ( 𝐴𝐺 ) )
3 mptmpoopabbrdOLD.y ( 𝜑𝑌 ∈ ( 𝐵𝐺 ) )
4 mptmpoopabbrdOLD.v ( 𝜑 → { ⟨ 𝑓 , ⟩ ∣ 𝜓 } ∈ 𝑉 )
5 mptmpoopabbrdOLD.r ( ( 𝜑𝑓 ( 𝐷𝐺 ) ) → 𝜓 )
6 mptmpoopabovdOLD.m 𝑀 = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( 𝐴𝑔 ) , 𝑏 ∈ ( 𝐵𝑔 ) ↦ { ⟨ 𝑓 , ⟩ ∣ ( 𝑓 ( 𝑎 ( 𝐶𝑔 ) 𝑏 ) 𝑓 ( 𝐷𝑔 ) ) } ) )
7 oveq12 ( ( 𝑎 = 𝑋𝑏 = 𝑌 ) → ( 𝑎 ( 𝐶𝐺 ) 𝑏 ) = ( 𝑋 ( 𝐶𝐺 ) 𝑌 ) )
8 7 breqd ( ( 𝑎 = 𝑋𝑏 = 𝑌 ) → ( 𝑓 ( 𝑎 ( 𝐶𝐺 ) 𝑏 ) 𝑓 ( 𝑋 ( 𝐶𝐺 ) 𝑌 ) ) )
9 fveq2 ( 𝑔 = 𝐺 → ( 𝐶𝑔 ) = ( 𝐶𝐺 ) )
10 9 oveqd ( 𝑔 = 𝐺 → ( 𝑎 ( 𝐶𝑔 ) 𝑏 ) = ( 𝑎 ( 𝐶𝐺 ) 𝑏 ) )
11 10 breqd ( 𝑔 = 𝐺 → ( 𝑓 ( 𝑎 ( 𝐶𝑔 ) 𝑏 ) 𝑓 ( 𝑎 ( 𝐶𝐺 ) 𝑏 ) ) )
12 1 2 3 4 5 8 11 6 mptmpoopabbrdOLD ( 𝜑 → ( 𝑋 ( 𝑀𝐺 ) 𝑌 ) = { ⟨ 𝑓 , ⟩ ∣ ( 𝑓 ( 𝑋 ( 𝐶𝐺 ) 𝑌 ) 𝑓 ( 𝐷𝐺 ) ) } )