Description: The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the object part of the composed functor. An object is mapped by two functors in succession. (Contributed by Zhi Wang, 3-Oct-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 >. >. ) |
||
| fuco111x.x | |- ( ph -> X e. ( Base ` C ) ) |
||
| Assertion | fuco111x | |- ( ph -> ( ( 1st ` ( O ` U ) ) ` X ) = ( K ` ( F ` X ) ) ) |
| 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 | fuco111x.x | |- ( ph -> X e. ( Base ` C ) ) |
|
| 6 | 1 2 3 4 | fuco111 | |- ( ph -> ( 1st ` ( O ` U ) ) = ( K o. F ) ) |
| 7 | 6 | fveq1d | |- ( ph -> ( ( 1st ` ( O ` U ) ) ` X ) = ( ( K o. F ) ` X ) ) |
| 8 | eqid | |- ( Base ` C ) = ( Base ` C ) |
|
| 9 | eqid | |- ( Base ` D ) = ( Base ` D ) |
|
| 10 | 8 9 2 | funcf1 | |- ( ph -> F : ( Base ` C ) --> ( Base ` D ) ) |
| 11 | 10 5 | fvco3d | |- ( ph -> ( ( K o. F ) ` X ) = ( K ` ( F ` X ) ) ) |
| 12 | 7 11 | eqtrd | |- ( ph -> ( ( 1st ` ( O ` U ) ) ` X ) = ( K ` ( F ` X ) ) ) |