Theorem mptmpoopabovd

Description: The operation value of a function value of a collection of ordered pairs of related elements. (Contributed by Alexander van der 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	|- ( ph -> G e. W )
	mptmpoopabbrd.x	|- ( ph -> X e. ( A ` G ) )
	mptmpoopabbrd.y	|- ( ph -> Y e. ( B ` G ) )
	mptmpoopabovd.m	|- M = ( g e. _V |-> ( a e. ( A ` g ) , b e. ( B ` g ) |-> { <. f , h >. | ( f ( a ( C ` g ) b ) h /\ f ( D ` g ) h ) } ) )
Assertion	mptmpoopabovd	|- ( ph -> ( X ( M ` G ) Y ) = { <. f , h >. | ( f ( X ( C ` G ) Y ) h /\ f ( D ` G ) h ) } )

Proof

Step	Hyp	Ref	Expression
1		mptmpoopabbrd.g	|- ( ph -> G e. W )
2		mptmpoopabbrd.x	|- ( ph -> X e. ( A ` G ) )
3		mptmpoopabbrd.y	|- ( ph -> Y e. ( B ` G ) )
4		mptmpoopabovd.m	|- M = ( g e. _V |-> ( a e. ( A ` g ) , b e. ( B ` g ) |-> { <. f , h >. | ( f ( a ( C ` g ) b ) h /\ f ( D ` g ) h ) } ) )
5		oveq12	|- ( ( a = X /\ b = Y ) -> ( a ( C ` G ) b ) = ( X ( C ` G ) Y ) )
6	5	breqd	|- ( ( a = X /\ b = Y ) -> ( f ( a ( C ` G ) b ) h <-> f ( X ( C ` G ) Y ) h ) )
7		fveq2	|- ( g = G -> ( C ` g ) = ( C ` G ) )
8	7	oveqd	|- ( g = G -> ( a ( C ` g ) b ) = ( a ( C ` G ) b ) )
9	8	breqd	|- ( g = G -> ( f ( a ( C ` g ) b ) h <-> f ( a ( C ` G ) b ) h ) )
10	1 2 3 6 9 4	mptmpoopabbrd	|- ( ph -> ( X ( M ` G ) Y ) = { <. f , h >. | ( f ( X ( C ` G ) Y ) h /\ f ( D ` G ) h ) } )