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	mptmpoopabbrdOLDOLD	⊢ ( 𝜑 → ( 𝑋 ( 𝑀 ‘ 𝐺 ) 𝑌 ) = { ⟨ 𝑓 , ℎ ⟩ ∣ ( 𝑓 ( 𝑋 ( 𝐶 ‘ 𝐺 ) 𝑌 ) ℎ ∧ 𝑓 ( 𝐷 ‘ 𝐺 ) ℎ ) } )