Metamath Proof Explorer

Theorem fuco11

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

Ref Expression
Hypotheses fuco11.o 
|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
fuco11.f 
|- ( ph -> F ( C Func D ) G )
fuco11.k 
|- ( ph -> K ( D Func E ) L )
fuco11.u 
|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
Assertion fuco11 
|- ( ph -> ( O ` U ) = ( <. K , L >. o.func <. F , G >. ) )

Proof

Step Hyp Ref Expression
1 fuco11.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
2 fuco11.f 
 |-  ( ph -> F ( C Func D ) G )
3 fuco11.k 
 |-  ( ph -> K ( D Func E ) L )
4 fuco11.u 
 |-  ( ph -> U = <. <. K , L >. , <. F , G >. >. )
5 2 funcrcl2 
 |-  ( ph -> C e. Cat )
6 3 funcrcl2 
 |-  ( ph -> D e. Cat )
7 3 funcrcl3 
 |-  ( ph -> E e. Cat )
8 eqidd 
 |-  ( ph -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
9 5 6 7 1 8 fuco1 
 |-  ( ph -> O = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) )
10 9 fveq1d 
 |-  ( ph -> ( O ` U ) = ( ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) ` U ) )
11 8 4 3 2 fuco2eld 
 |-  ( ph -> U e. ( ( D Func E ) X. ( C Func D ) ) )
12 11 fvresd 
 |-  ( ph -> ( ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) ` U ) = ( o.func ` U ) )
13 4 fveq2d 
 |-  ( ph -> ( o.func ` U ) = ( o.func ` <. <. K , L >. , <. F , G >. >. ) )
14 df-ov 
 |-  ( <. K , L >. o.func <. F , G >. ) = ( o.func ` <. <. K , L >. , <. F , G >. >. )
15 13 14 eqtr4di 
 |-  ( ph -> ( o.func ` U ) = ( <. K , L >. o.func <. F , G >. ) )
16 10 12 15 3eqtrd 
 |-  ( ph -> ( O ` U ) = ( <. K , L >. o.func <. F , G >. ) )