Theorem termcpostfix

Description: Post-composition by an object-fixing endofunctor induces an object-fixing endofunctor on a functor category with terminal source. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	termcfunc1eq.c	|- ( ph -> C e. TermCat )
	termcpostfix.q	|- Q = ( C FuncCat D )
	termcpostfix.r	|- R = ( D FuncCat D )
	termcpostfix.o	|- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F D ) )
	termcpostfix.k	|- K = ( ( 1st ` .o. ) ` F )
	termcpostfix.f	|- ( ph -> F e. ( D Func D ) )
	termcpostfix.i	|- ( ph -> ( 1st ` F ) = ( _I |` A ) )
Assertion	termcpostfix	|- ( ph -> ( K e. ( Q Func Q ) /\ ( 1st ` K ) = ( _I |` ( C Func D ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		termcfunc1eq.c	|- ( ph -> C e. TermCat )
2		termcpostfix.q	|- Q = ( C FuncCat D )
3		termcpostfix.r	|- R = ( D FuncCat D )
4		termcpostfix.o	|- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F D ) )
5		termcpostfix.k	|- K = ( ( 1st ` .o. ) ` F )
6		termcpostfix.f	|- ( ph -> F e. ( D Func D ) )
7		termcpostfix.i	|- ( ph -> ( 1st ` F ) = ( _I |` A ) )
8	1	termccatd	|- ( ph -> C e. Cat )
9	2 3 4 6 8 5 2	postcofcl	|- ( ph -> K e. ( Q Func Q ) )
10	2 3 4 6 8 5	postcof1st	|- ( ph -> ( 1st ` K ) = ( g e. ( C Func D ) |-> ( F o.func g ) ) )
11	1	adantr	|- ( ( ph /\ g e. ( C Func D ) ) -> C e. TermCat )
12		simpr	|- ( ( ph /\ g e. ( C Func D ) ) -> g e. ( C Func D ) )
13	6	adantr	|- ( ( ph /\ g e. ( C Func D ) ) -> F e. ( D Func D ) )
14	7	adantr	|- ( ( ph /\ g e. ( C Func D ) ) -> ( 1st ` F ) = ( _I |` A ) )
15	11 12 13 14	termccofix	|- ( ( ph /\ g e. ( C Func D ) ) -> ( F o.func g ) = g )
16	15	mpteq2dva	|- ( ph -> ( g e. ( C Func D ) |-> ( F o.func g ) ) = ( g e. ( C Func D ) |-> g ) )
17	10 16	eqtrd	|- ( ph -> ( 1st ` K ) = ( g e. ( C Func D ) |-> g ) )
18		mptresid	|- ( _I |` ( C Func D ) ) = ( g e. ( C Func D ) |-> g )
19	17 18	eqtr4di	|- ( ph -> ( 1st ` K ) = ( _I |` ( C Func D ) ) )
20	9 19	jca	|- ( ph -> ( K e. ( Q Func Q ) /\ ( 1st ` K ) = ( _I |` ( C Func D ) ) ) )