This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cofu1st2nd

Description: Rewrite the functor composition with separated functor parts. (Contributed by Zhi Wang, 15-Nov-2025)

Ref Expression
Hypotheses cofu1st2nd.f 
|- ( ph -> F e. ( C Func D ) )
cofu1st2nd.g 
|- ( ph -> G e. ( D Func E ) )
Assertion cofu1st2nd 
|- ( ph -> ( G o.func F ) = ( <. ( 1st ` G ) , ( 2nd ` G ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) )

Proof

Step Hyp Ref Expression
1 cofu1st2nd.f 
 |-  ( ph -> F e. ( C Func D ) )
2 cofu1st2nd.g 
 |-  ( ph -> G e. ( D Func E ) )
3 relfunc 
 |-  Rel ( D Func E )
4 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ G e. ( D Func E ) ) -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
5 3 2 4 sylancr 
 |-  ( ph -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
6 relfunc 
 |-  Rel ( C Func D )
7 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
8 6 1 7 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
9 5 8 oveq12d 
 |-  ( ph -> ( G o.func F ) = ( <. ( 1st ` G ) , ( 2nd ` G ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) )