Metamath Proof Explorer


Theorem mptmpoopabovdOLD

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

Proof

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