Theorem fuco11a

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	No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
	fuco11.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
	fuco11.k	$$⊢\phi \to K\left(D\mathrm{Func}E\right)L$$
	fuco11.u	$$⊢\phi \to U=⟨⟨K,L⟩,⟨F,G⟩⟩$$
	fuco11a.b	$$⊢B={\mathrm{Base}}_C$$
Assertion	fuco11a	$$⊢\phi \to O\left(U\right)=⟨K\circ F,\left(x\in B,y\in B⟼\left(F\left(x\right)LF\left(y\right)\right)\circ \left(xGy\right)\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		fuco11.o	Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
2		fuco11.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
3		fuco11.k	$$⊢\phi \to K\left(D\mathrm{Func}E\right)L$$
4		fuco11.u	$$⊢\phi \to U=⟨⟨K,L⟩,⟨F,G⟩⟩$$
5		fuco11a.b	$$⊢B={\mathrm{Base}}_C$$
6	1 2 3 4	fuco11	$$⊢\phi \to O\left(U\right)=⟨K,L⟩{\circ }_{\mathrm{func}}⟨F,G⟩$$
7	5 2 3	cofuval2	$$⊢\phi \to ⟨K,L⟩{\circ }_{\mathrm{func}}⟨F,G⟩=⟨K\circ F,\left(x\in B,y\in B⟼\left(F\left(x\right)LF\left(y\right)\right)\circ \left(xGy\right)\right)⟩$$
8	6 7	eqtrd	$$⊢\phi \to O\left(U\right)=⟨K\circ F,\left(x\in B,y\in B⟼\left(F\left(x\right)LF\left(y\right)\right)\circ \left(xGy\right)\right)⟩$$