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) 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 ) } )