Description: The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly. (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 >. >. ) |
||
| fuco11a.b | |- B = ( Base ` C ) |
||
| Assertion | fuco11a | |- ( ph -> ( O ` U ) = <. ( K o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. ) |
| 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 | fuco11a.b | |- B = ( Base ` C ) |
|
| 6 | 1 2 3 4 | fuco11 | |- ( ph -> ( O ` U ) = ( <. K , L >. o.func <. F , G >. ) ) |
| 7 | 5 2 3 | cofuval2 | |- ( ph -> ( <. K , L >. o.func <. F , G >. ) = <. ( K o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. ) |
| 8 | 6 7 | eqtrd | |- ( ph -> ( O ` U ) = <. ( K o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. ) |