Metamath Proof Explorer

Theorem fuco11b

Description: The object part of the functor composition bifunctor maps two functors to their composition. (Contributed by Zhi Wang, 11-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 fuco11b.o 
 |-  ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = O )
2 fuco11b.f 
 |-  ( ph -> F e. ( C Func D ) )
3 fuco11b.g 
 |-  ( ph -> G e. ( D Func E ) )
4 relfunc 
 |-  Rel ( C Func D )
5 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
6 4 2 5 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
7 6 funcrcl2 
 |-  ( ph -> C e. Cat )
8 relfunc 
 |-  Rel ( D Func E )
9 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ G e. ( D Func E ) ) -> ( 1st ` G ) ( D Func E ) ( 2nd ` G ) )
10 8 3 9 sylancr 
 |-  ( ph -> ( 1st ` G ) ( D Func E ) ( 2nd ` G ) )
11 10 funcrcl2 
 |-  ( ph -> D e. Cat )
12 10 funcrcl3 
 |-  ( ph -> E e. Cat )
13 eqidd 
 |-  ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) )
14 7 11 12 13 fucoelvv 
 |-  ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) )
15 1st2nd2 
 |-  ( ( <. C , D >. o.F E ) e. ( _V X. _V ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. )
16 14 15 syl 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. )
17 eqidd 
 |-  ( ph -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
18 7 11 12 16 17 fuco1 
 |-  ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) )
19 1 18 eqtr3d 
 |-  ( ph -> O = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) )
20 19 oveqd 
 |-  ( ph -> ( G O F ) = ( G ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) F ) )
21 ovres 
 |-  ( ( G e. ( D Func E ) /\ F e. ( C Func D ) ) -> ( G ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) F ) = ( G o.func F ) )
22 3 2 21 syl2anc 
 |-  ( ph -> ( G ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) F ) = ( G o.func F ) )
23 20 22 eqtrd 
 |-  ( ph -> ( G O F ) = ( G o.func F ) )