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