Theorem fucof1

Description: The object part of the functor composition bifunctor maps ( ( D Func E ) X. ( C Func D ) ) into ( C Func E ) . (Contributed by Zhi Wang, 29-Sep-2025)

	Ref	Expression
Hypotheses	fucofval.c	|- ( ph -> C e. T )
	fucofval.d	|- ( ph -> D e. U )
	fucofval.e	|- ( ph -> E e. V )
	fuco1.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
	fuco1.w	|- ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
Assertion	fucof1	|- ( ph -> O : W --> ( C Func E ) )

Proof

Step	Hyp	Ref	Expression
1		fucofval.c	|- ( ph -> C e. T )
2		fucofval.d	|- ( ph -> D e. U )
3		fucofval.e	|- ( ph -> E e. V )
4		fuco1.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
5		fuco1.w	|- ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
6		rescofuf	|- ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) : ( ( D Func E ) X. ( C Func D ) ) --> ( C Func E )
7	1 2 3 4 5	fuco1	|- ( ph -> O = ( o.func |` W ) )
8	5	reseq2d	|- ( ph -> ( o.func |` W ) = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) )
9	7 8	eqtrd	|- ( ph -> O = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) )
10	9 5	feq12d	|- ( ph -> ( O : W --> ( C Func E ) <-> ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) : ( ( D Func E ) X. ( C Func D ) ) --> ( C Func E ) ) )
11	6 10	mpbiri	|- ( ph -> O : W --> ( C Func E ) )