Theorem fucoaltfunc

Description: Post-compose functor composition with an object-fixing endofunctor of its target. The original object function remains literally fixed for arbitrary source and intermediate categories. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	fucoaltfunc.q	|- Q = ( C FuncCat E )
	fucoaltfunc.t	|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
	fucoaltfunc.l	|- L = ( <. C , D >. o.F E )
	fucoaltfunc.c	|- ( ph -> C e. Cat )
	fucoaltfunc.d	|- ( ph -> D e. Cat )
	fucoaltfunc.e	|- ( ph -> E e. Cat )
	fucoaltfunc.k	|- ( ph -> K e. ( Q Func Q ) )
	fucoaltfunc.i	|- ( ph -> ( 1st ` K ) = ( _I |` ( C Func E ) ) )
Assertion	fucoaltfunc	|- ( ph -> ( 1st ` L ) ( T Func Q ) ( 2nd ` ( K o.func L ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoaltfunc.q	|- Q = ( C FuncCat E )
2		fucoaltfunc.t	|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
3		fucoaltfunc.l	|- L = ( <. C , D >. o.F E )
4		fucoaltfunc.c	|- ( ph -> C e. Cat )
5		fucoaltfunc.d	|- ( ph -> D e. Cat )
6		fucoaltfunc.e	|- ( ph -> E e. Cat )
7		fucoaltfunc.k	|- ( ph -> K e. ( Q Func Q ) )
8		fucoaltfunc.i	|- ( ph -> ( 1st ` K ) = ( _I |` ( C Func E ) ) )
9	1	fucbas	|- ( C Func E ) = ( Base ` Q )
10	2 1 4 5 6	fucofunca	|- ( ph -> ( <. C , D >. o.F E ) e. ( T Func Q ) )
11	3 10	eqeltrid	|- ( ph -> L e. ( T Func Q ) )
12	9 11 7 8	cofu1stfix	|- ( ph -> ( 1st ` ( K o.func L ) ) = ( 1st ` L ) )
13	11 7	cofucl	|- ( ph -> ( K o.func L ) e. ( T Func Q ) )
14	13	func1st2nd	|- ( ph -> ( 1st ` ( K o.func L ) ) ( T Func Q ) ( 2nd ` ( K o.func L ) ) )
15	12 14	breq1dd	|- ( ph -> ( 1st ` L ) ( T Func Q ) ( 2nd ` ( K o.func L ) ) )