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		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
5		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
6	4 2 5	sylancr	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
7	6	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
8		relfunc	$$⊢\mathrm{Rel}\left(D\mathrm{Func}E\right)$$
9		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(D\mathrm{Func}E\right)\wedge G\in \left(D\mathrm{Func}E\right)\right)\to 1^{st}\left(G\right)\left(D\mathrm{Func}E\right)2^{nd}\left(G\right)$$
10	8 3 9	sylancr	$$⊢\phi \to 1^{st}\left(G\right)\left(D\mathrm{Func}E\right)2^{nd}\left(G\right)$$
11	10	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
12	10	funcrcl3	$$⊢\phi \to E\in \mathrm{Cat}$$
13		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 |-
14	7 11 12 13	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 |-
15		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 |-
16	14 15	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 |-
17		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)$$
18	7 11 12 16 17	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 |-
19	1 18	eqtr3d	$$⊢\phi \to O={{\circ }_{\mathrm{func}}\upharpoonright }_{\left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)}$$
20	19	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$$
21		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$$
22	3 2 21	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$$
23	20 22	eqtrd	$$⊢\phi \to GOF=G{\circ }_{\mathrm{func}}F$$