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	|- ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = O )
	fuco11b.f	|- ( ph -> F e. ( C Func D ) )
	fuco11b.g	|- ( ph -> G e. ( D Func E ) )
Assertion	fuco11b	|- ( ph -> ( G O F ) = ( G o.func F ) )

Proof

Step	Hyp	Ref	Expression
1		fuco11b.o	|- ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = O )
2		fuco11b.f	|- ( ph -> F e. ( C Func D ) )
3		fuco11b.g	|- ( ph -> G e. ( D Func E ) )
4	2	func1st2nd	|- ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
5	4	funcrcl2	|- ( ph -> C e. Cat )
6	3	func1st2nd	|- ( ph -> ( 1st ` G ) ( D Func E ) ( 2nd ` G ) )
7	6	funcrcl2	|- ( ph -> D e. Cat )
8	6	funcrcl3	|- ( ph -> E e. Cat )
9		eqidd	|- ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) )
10	5 7 8 9	fucoelvv	|- ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) )
11		1st2nd2	|- ( ( <. 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 ) ) >. )
12	10 11	syl	|- ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. )
13		eqidd	|- ( ph -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
14	5 7 8 12 13	fuco1	|- ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) )
15	1 14	eqtr3d	|- ( ph -> O = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) )
16	15	oveqd	|- ( ph -> ( G O F ) = ( G ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) F ) )
17		ovres	|- ( ( G e. ( D Func E ) /\ F e. ( C Func D ) ) -> ( G ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) F ) = ( G o.func F ) )
18	3 2 17	syl2anc	|- ( ph -> ( G ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) F ) = ( G o.func F ) )
19	16 18	eqtrd	|- ( ph -> ( G O F ) = ( G o.func F ) )