Theorem fuco111

Description: The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the object part of the composed functor. (Contributed by Zhi Wang, 2-Oct-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 >. >. )
Assertion	fuco111	|- ( ph -> ( 1st ` ( O ` U ) ) = ( K o. F ) )

Proof

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		eqid	|- ( Base ` C ) = ( Base ` C )
6	1 2 3 4 5	fuco11a	|- ( ph -> ( O ` U ) = <. ( K o. F ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. )
7	6	fveq2d	|- ( ph -> ( 1st ` ( O ` U ) ) = ( 1st ` <. ( K o. F ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. ) )
8		relfunc	|- Rel ( D Func E )
9	8	brrelex1i	|- ( K ( D Func E ) L -> K e. _V )
10	3 9	syl	|- ( ph -> K e. _V )
11		relfunc	|- Rel ( C Func D )
12	11	brrelex1i	|- ( F ( C Func D ) G -> F e. _V )
13	2 12	syl	|- ( ph -> F e. _V )
14	10 13	coexd	|- ( ph -> ( K o. F ) e. _V )
15		fvex	|- ( Base ` C ) e. _V
16	15 15	mpoex	|- ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) e. _V
17		op1stg	|- ( ( ( K o. F ) e. _V /\ ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) e. _V ) -> ( 1st ` <. ( K o. F ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. ) = ( K o. F ) )
18	14 16 17	sylancl	|- ( ph -> ( 1st ` <. ( K o. F ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. ) = ( K o. F ) )
19	7 18	eqtrd	|- ( ph -> ( 1st ` ( O ` U ) ) = ( K o. F ) )