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 |
|
mptmpoopabovd.m |
|- M = ( g e. _V |-> ( a e. ( A ` g ) , b e. ( B ` g ) |-> { <. f , h >. | ( f ( a ( C ` g ) b ) h /\ f ( D ` g ) h ) } ) ) |
7 |
|
oveq12 |
|- ( ( a = X /\ b = Y ) -> ( a ( C ` G ) b ) = ( X ( C ` G ) Y ) ) |
8 |
7
|
breqd |
|- ( ( a = X /\ b = Y ) -> ( f ( a ( C ` G ) b ) h <-> f ( X ( C ` G ) Y ) h ) ) |
9 |
|
fveq2 |
|- ( g = G -> ( C ` g ) = ( C ` G ) ) |
10 |
9
|
oveqd |
|- ( g = G -> ( a ( C ` g ) b ) = ( a ( C ` G ) b ) ) |
11 |
10
|
breqd |
|- ( g = G -> ( f ( a ( C ` g ) b ) h <-> f ( a ( C ` G ) b ) h ) ) |
12 |
1 2 3 4 5 8 11 6
|
mptmpoopabbrd |
|- ( ph -> ( X ( M ` G ) Y ) = { <. f , h >. | ( f ( X ( C ` G ) Y ) h /\ f ( D ` G ) h ) } ) |