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	No typesetting found for |- ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = O ) with typecode |-
	fuco11b.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	fuco11b.g	$$⊢\phi \to G\in \left(D\mathrm{Func}E\right)$$
Assertion	fuco11b	$$⊢\phi \to GOF=G{\circ }_{\mathrm{func}}F$$

Proof

Step	Hyp	Ref	Expression
1		fuco11b.o	Could not format ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = O ) : No typesetting found for |- ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = O ) with typecode |-
2		fuco11b.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
3		fuco11b.g	$$⊢\phi \to G\in \left(D\mathrm{Func}E\right)$$
4	2	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
5	4	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
6	3	func1st2nd	$$⊢\phi \to 1^{st}\left(G\right)\left(D\mathrm{Func}E\right)2^{nd}\left(G\right)$$
7	6	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
8	6	funcrcl3	$$⊢\phi \to E\in \mathrm{Cat}$$
9		eqidd	Could not format ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) ) with typecode |-
10	5 7 8 9	fucoelvv	Could not format ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) ) with typecode |-
11		1st2nd2	Could not format ( ( <. 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 ) ) >. ) : No typesetting found for |- ( ( <. 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 ) ) >. ) with typecode |-
12	10 11	syl	Could not format ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) with typecode |-
13		eqidd	$$⊢\phi \to \left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)=\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)$$
14	5 7 8 12 13	fuco1	Could not format ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) ) : No typesetting found for |- ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) ) with typecode |-
15	1 14	eqtr3d	$$⊢\phi \to O={{\circ }_{\mathrm{func}}\upharpoonright }_{\left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)}$$
16	15	oveqd	$$⊢\phi \to GOF=G\left({{\circ }_{\mathrm{func}}\upharpoonright }_{\left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)}\right)F$$
17		ovres	$$⊢\left(G\in \left(D\mathrm{Func}E\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to G\left({{\circ }_{\mathrm{func}}\upharpoonright }_{\left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)}\right)F=G{\circ }_{\mathrm{func}}F$$
18	3 2 17	syl2anc	$$⊢\phi \to G\left({{\circ }_{\mathrm{func}}\upharpoonright }_{\left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)}\right)F=G{\circ }_{\mathrm{func}}F$$
19	16 18	eqtrd	$$⊢\phi \to GOF=G{\circ }_{\mathrm{func}}F$$