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 |
15 16
|
mpoex |
|- ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) e. _V |
18 |
17
|
a1i |
|- ( ph -> ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) e. _V ) |
19 |
6 13 14 18
|
fvmptd3 |
|- ( ph -> ( M ` G ) = ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) ) |
20 |
19
|
oveqd |
|- ( ph -> ( X ( M ` G ) Y ) = ( X ( a e. ( A ` G ) , b e. ( B ` G ) |-> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } ) Y ) ) |
21 |
4
|
anbi1d |
|- ( ( a = X /\ b = Y ) -> ( ( ta /\ f ( D ` G ) h ) <-> ( th /\ f ( D ` G ) h ) ) ) |
22 |
21
|
opabbidv |
|- ( ( a = X /\ b = Y ) -> { <. f , h >. | ( ta /\ f ( D ` G ) h ) } = { <. f , h >. | ( th /\ f ( D ` G ) h ) } ) |
23 |
|
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 ) } ) |
24 |
|
ancom |
|- ( ( th /\ f ( D ` G ) h ) <-> ( f ( D ` G ) h /\ th ) ) |
25 |
24
|
opabbii |
|- { <. f , h >. | ( th /\ f ( D ` G ) h ) } = { <. f , h >. | ( f ( D ` G ) h /\ th ) } |
26 |
|
opabresex2 |
|- { <. f , h >. | ( f ( D ` G ) h /\ th ) } e. _V |
27 |
25 26
|
eqeltri |
|- { <. f , h >. | ( th /\ f ( D ` G ) h ) } e. _V |
28 |
22 23 27
|
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 ) } ) |
29 |
2 3 28
|
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 ) } ) |
30 |
20 29
|
eqtrd |
|- ( ph -> ( X ( M ` G ) Y ) = { <. f , h >. | ( th /\ f ( D ` G ) h ) } ) |