Description: Obsolete version of mptmpoopabovd as of 13-Dec-2024. (Contributed by Alexander van der Vekens, 8-Nov-2017) (Revised by AV, 15-Jan-2021) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mptmpoopabbrdOLD.g | |- ( ph -> G e. W ) |
|
mptmpoopabbrdOLD.x | |- ( ph -> X e. ( A ` G ) ) |
||
mptmpoopabbrdOLD.y | |- ( ph -> Y e. ( B ` G ) ) |
||
mptmpoopabbrdOLD.v | |- ( ph -> { <. f , h >. | ps } e. V ) |
||
mptmpoopabbrdOLD.r | |- ( ( ph /\ f ( D ` G ) h ) -> ps ) |
||
mptmpoopabovdOLD.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 ) } ) ) |
||
Assertion | mptmpoopabovdOLD | |- ( ph -> ( X ( M ` G ) Y ) = { <. f , h >. | ( f ( X ( C ` G ) Y ) h /\ f ( D ` G ) h ) } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mptmpoopabbrdOLD.g | |- ( ph -> G e. W ) |
|
2 | mptmpoopabbrdOLD.x | |- ( ph -> X e. ( A ` G ) ) |
|
3 | mptmpoopabbrdOLD.y | |- ( ph -> Y e. ( B ` G ) ) |
|
4 | mptmpoopabbrdOLD.v | |- ( ph -> { <. f , h >. | ps } e. V ) |
|
5 | mptmpoopabbrdOLD.r | |- ( ( ph /\ f ( D ` G ) h ) -> ps ) |
|
6 | mptmpoopabovdOLD.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 | mptmpoopabbrdOLD | |- ( ph -> ( X ( M ` G ) Y ) = { <. f , h >. | ( f ( X ( C ` G ) Y ) h /\ f ( D ` G ) h ) } ) |