Theorem cofu1a

Description: Value of the object part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025)

	Ref	Expression
Hypotheses	cofu1a.b	|- B = ( Base ` C )
	cofu1a.f	|- ( ph -> F ( C Func D ) G )
	cofu1a.k	|- ( ph -> K ( D Func E ) L )
	cofu1a.m	|- ( ph -> ( <. K , L >. o.func <. F , G >. ) = <. M , N >. )
	cofu1a.x	|- ( ph -> X e. B )
Assertion	cofu1a	|- ( ph -> ( K ` ( F ` X ) ) = ( M ` X ) )

Proof

Step	Hyp	Ref	Expression
1		cofu1a.b	|- B = ( Base ` C )
2		cofu1a.f	|- ( ph -> F ( C Func D ) G )
3		cofu1a.k	|- ( ph -> K ( D Func E ) L )
4		cofu1a.m	|- ( ph -> ( <. K , L >. o.func <. F , G >. ) = <. M , N >. )
5		cofu1a.x	|- ( ph -> X e. B )
6		df-br	|- ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
7	2 6	sylib	|- ( ph -> <. F , G >. e. ( C Func D ) )
8		df-br	|- ( K ( D Func E ) L <-> <. K , L >. e. ( D Func E ) )
9	3 8	sylib	|- ( ph -> <. K , L >. e. ( D Func E ) )
10	1 7 9 5	cofu1	|- ( ph -> ( ( 1st ` ( <. K , L >. o.func <. F , G >. ) ) ` X ) = ( ( 1st ` <. K , L >. ) ` ( ( 1st ` <. F , G >. ) ` X ) ) )
11	4	fveq2d	|- ( ph -> ( 1st ` ( <. K , L >. o.func <. F , G >. ) ) = ( 1st ` <. M , N >. ) )
12	7 9	cofucl	|- ( ph -> ( <. K , L >. o.func <. F , G >. ) e. ( C Func E ) )
13	4 12	eqeltrrd	|- ( ph -> <. M , N >. e. ( C Func E ) )
14		df-br	|- ( M ( C Func E ) N <-> <. M , N >. e. ( C Func E ) )
15	13 14	sylibr	|- ( ph -> M ( C Func E ) N )
16	15	func1st	|- ( ph -> ( 1st ` <. M , N >. ) = M )
17	11 16	eqtrd	|- ( ph -> ( 1st ` ( <. K , L >. o.func <. F , G >. ) ) = M )
18	17	fveq1d	|- ( ph -> ( ( 1st ` ( <. K , L >. o.func <. F , G >. ) ) ` X ) = ( M ` X ) )
19	3	func1st	|- ( ph -> ( 1st ` <. K , L >. ) = K )
20	2	func1st	|- ( ph -> ( 1st ` <. F , G >. ) = F )
21	20	fveq1d	|- ( ph -> ( ( 1st ` <. F , G >. ) ` X ) = ( F ` X ) )
22	19 21	fveq12d	|- ( ph -> ( ( 1st ` <. K , L >. ) ` ( ( 1st ` <. F , G >. ) ` X ) ) = ( K ` ( F ` X ) ) )
23	10 18 22	3eqtr3rd	|- ( ph -> ( K ` ( F ` X ) ) = ( M ` X ) )