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	|- ( ph -> G e. W )
	mptmpoopabbrd.x	|- ( ph -> X e. ( A ` G ) )
	mptmpoopabbrd.y	|- ( ph -> Y e. ( B ` G ) )
	mptmpoopabbrd.1	|- ( ( a = X /\ b = Y ) -> ( ta <-> th ) )
	mptmpoopabbrd.2	|- ( g = G -> ( ch <-> ta ) )
	mptmpoopabbrd.m	|- M = ( g e. _V |-> ( a e. ( A ` g ) , b e. ( B ` g ) |-> { <. f , h >. | ( ch /\ f ( D ` g ) h ) } ) )
Assertion	mptmpoopabbrd	|- ( ph -> ( X ( M ` G ) Y ) = { <. f , h >. | ( th /\ 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		mptmpoopabbrd.1	|- ( ( a = X /\ b = Y ) -> ( ta <-> th ) )
5		mptmpoopabbrd.2	|- ( g = G -> ( ch <-> ta ) )
6		mptmpoopabbrd.m	|- M = ( g e. _V |-> ( a e. ( A ` g ) , b e. ( B ` g ) |-> { <. f , h >. | ( ch /\ f ( D ` g ) h ) } ) )
7		fveq2	|- ( g = G -> ( A ` g ) = ( A ` G ) )
8		fveq2	|- ( g = G -> ( B ` g ) = ( B ` G ) )
9		fveq2	|- ( g = G -> ( D ` g ) = ( D ` G ) )
10	9	breqd	|- ( g = G -> ( f ( D ` g ) h <-> f ( D ` G ) h ) )
11	5 10	anbi12d	|- ( g = G -> ( ( ch /\ f ( D ` g ) h ) <-> ( ta /\ f ( D ` G ) h ) ) )
12	11	opabbidv	|- ( g = G -> { <. f , h >. | ( ch /\ f ( D ` g ) h ) } = { <. f , h >. | ( ta /\ f ( D ` G ) h ) } )
13	7 8 12	mpoeq123dv	|- ( g = G -> ( a e. ( A ` g ) , b e. ( B ` g ) |-> { <. f , h >. | ( ch /\ f ( D ` g ) h ) } ) = ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) )
14	1	elexd	|- ( ph -> G e. _V )
15		fvex	|- ( A ` G ) e. _V
16		fvex	|- ( B ` G ) e. _V
17		fvex	|- ( D ` G ) e. _V
18	17	pwex	|- ~P ( D ` G ) e. _V
19		simpr	|- ( ( ta /\ f ( D ` G ) h ) -> f ( D ` G ) h )
20	19	ssopab2i	|- { <. f , h >. | ( ta /\ f ( D ` G ) h ) } C_ { <. f , h >. | f ( D ` G ) h }
21		opabss	|- { <. f , h >. | f ( D ` G ) h } C_ ( D ` G )
22	20 21	sstri	|- { <. f , h >. | ( ta /\ f ( D ` G ) h ) } C_ ( D ` G )
23	17 22	elpwi2	|- { <. f , h >. | ( ta /\ f ( D ` G ) h ) } e. ~P ( D ` G )
24	23	rgen2w	|- A. a e. ( A ` G ) A. b e. ( B ` G ) { <. f , h >. | ( ta /\ f ( D ` G ) h ) } e. ~P ( D ` G )
25	15 16 18 24	mpoexw	|- ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) e. _V
26	25	a1i	|- ( ph -> ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) e. _V )
27	6 13 14 26	fvmptd3	|- ( ph -> ( M ` G ) = ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) )
28	27	oveqd	|- ( ph -> ( X ( M ` G ) Y ) = ( X ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) Y ) )
29	4	anbi1d	|- ( ( a = X /\ b = Y ) -> ( ( ta /\ f ( D ` G ) h ) <-> ( th /\ f ( D ` G ) h ) ) )
30	29	opabbidv	|- ( ( a = X /\ b = Y ) -> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } = { <. f , h >. | ( th /\ f ( D ` G ) h ) } )
31		eqid	|- ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) = ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } )
32		ancom	|- ( ( th /\ f ( D ` G ) h ) <-> ( f ( D ` G ) h /\ th ) )
33	32	opabbii	|- { <. f , h >. | ( th /\ f ( D ` G ) h ) } = { <. f , h >. | ( f ( D ` G ) h /\ th ) }
34		opabresex2	|- { <. f , h >. | ( f ( D ` G ) h /\ th ) } e. _V
35	33 34	eqeltri	|- { <. f , h >. | ( th /\ f ( D ` G ) h ) } e. _V
36	30 31 35	ovmpoa	|- ( ( X e. ( A ` G ) /\ Y e. ( B ` G ) ) -> ( X ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) Y ) = { <. f , h >. | ( th /\ f ( D ` G ) h ) } )
37	2 3 36	syl2anc	|- ( ph -> ( X ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) Y ) = { <. f , h >. | ( th /\ f ( D ` G ) h ) } )
38	28 37	eqtrd	|- ( ph -> ( X ( M ` G ) Y ) = { <. f , h >. | ( th /\ f ( D ` G ) h ) } )