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)

Ref Expression
Hypotheses mptmpoopabbrd.g 
|- ( ph -> G e. W )
mptmpoopabbrd.x 
|- ( ph -> X e. ( A ` G ) )
mptmpoopabbrd.y 
|- ( ph -> Y e. ( B ` G ) )
mptmpoopabbrd.v 
|- ( ph -> { <. f , h >. | ps } e. V )
mptmpoopabbrd.r 
|- ( ( ph /\ f ( D ` G ) h ) -> ps )
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.v 
 |-  ( ph -> { <. f , h >. | ps } e. V )
5 mptmpoopabbrd.r 
 |-  ( ( ph /\ f ( D ` G ) h ) -> ps )
6 mptmpoopabbrd.1 
 |-  ( ( a = X /\ b = Y ) -> ( ta <-> th ) )
7 mptmpoopabbrd.2 
 |-  ( g = G -> ( ch <-> ta ) )
8 mptmpoopabbrd.m 
 |-  M = ( g e. _V |-> ( a e. ( A ` g ) , b e. ( B ` g ) |-> { <. f , h >. | ( ch /\ f ( D ` g ) h ) } ) )
9 fveq2 
 |-  ( g = G -> ( A ` g ) = ( A ` G ) )
10 fveq2 
 |-  ( g = G -> ( B ` g ) = ( B ` G ) )
11 fveq2 
 |-  ( g = G -> ( D ` g ) = ( D ` G ) )
12 11 breqd 
 |-  ( g = G -> ( f ( D ` g ) h <-> f ( D ` G ) h ) )
13 7 12 anbi12d 
 |-  ( g = G -> ( ( ch /\ f ( D ` g ) h ) <-> ( ta /\ f ( D ` G ) h ) ) )
14 13 opabbidv 
 |-  ( g = G -> { <. f , h >. | ( ch /\ f ( D ` g ) h ) } = { <. f , h >. | ( ta /\ f ( D ` G ) h ) } )
15 9 10 14 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 ) } ) )
16 elex 
 |-  ( G e. W -> G e. _V )
17 16 adantr 
 |-  ( ( G e. W /\ G e. W ) -> G e. _V )
18 fvex 
 |-  ( A ` G ) e. _V
19 fvex 
 |-  ( B ` G ) e. _V
20 18 19 pm3.2i 
 |-  ( ( A ` G ) e. _V /\ ( B ` G ) e. _V )
21 mpoexga 
 |-  ( ( ( A ` G ) e. _V /\ ( B ` G ) e. _V ) -> ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) e. _V )
22 20 21 mp1i 
 |-  ( ( G e. W /\ G e. W ) -> ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) e. _V )
23 8 15 17 22 fvmptd3 
 |-  ( ( G e. W /\ G e. W ) -> ( M ` G ) = ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) )
24 1 1 23 syl2anc 
 |-  ( ph -> ( M ` G ) = ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) )
25 24 oveqd 
 |-  ( ph -> ( X ( M ` G ) Y ) = ( X ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) Y ) )
26 ancom 
 |-  ( ( th /\ f ( D ` G ) h ) <-> ( f ( D ` G ) h /\ th ) )
27 26 opabbii 
 |-  { <. f , h >. | ( th /\ f ( D ` G ) h ) } = { <. f , h >. | ( f ( D ` G ) h /\ th ) }
28 5 4 opabresex2d 
 |-  ( ph -> { <. f , h >. | ( f ( D ` G ) h /\ th ) } e. _V )
29 27 28 eqeltrid 
 |-  ( ph -> { <. f , h >. | ( th /\ f ( D ` G ) h ) } e. _V )
30 6 anbi1d 
 |-  ( ( a = X /\ b = Y ) -> ( ( ta /\ f ( D ` G ) h ) <-> ( th /\ f ( D ` G ) h ) ) )
31 30 opabbidv 
 |-  ( ( a = X /\ b = Y ) -> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } = { <. f , h >. | ( th /\ f ( D ` G ) h ) } )
32 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 ) } )
33 31 32 ovmpoga 
 |-  ( ( X e. ( A ` G ) /\ Y e. ( B ` G ) /\ { <. f , h >. | ( th /\ f ( D ` G ) h ) } e. _V ) -> ( X ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) Y ) = { <. f , h >. | ( th /\ f ( D ` G ) h ) } )
34 2 3 29 33 syl3anc 
 |-  ( 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 ) } )
35 25 34 eqtrd 
 |-  ( ph -> ( X ( M ` G ) Y ) = { <. f , h >. | ( th /\ f ( D ` G ) h ) } )