Theorem cofuterm

Description: Post-compose with a functor to a terminal category. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	cofuterm.f	|- ( ph -> F e. ( C Func D ) )
	cofuterm.g	|- ( ph -> G e. ( D Func E ) )
	cofuterm.k	|- ( ph -> K e. ( C Func E ) )
	cofuterm.e	|- ( ph -> E e. TermCat )
Assertion	cofuterm	|- ( ph -> ( G o.func F ) = K )

Proof

Step	Hyp	Ref	Expression
1		cofuterm.f	|- ( ph -> F e. ( C Func D ) )
2		cofuterm.g	|- ( ph -> G e. ( D Func E ) )
3		cofuterm.k	|- ( ph -> K e. ( C Func E ) )
4		cofuterm.e	|- ( ph -> E e. TermCat )
5		eqid	|- ( C FuncCat E ) = ( C FuncCat E )
6	1	func1st2nd	|- ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
7	6	funcrcl2	|- ( ph -> C e. Cat )
8	5 7 4	fucterm	|- ( ph -> ( C FuncCat E ) e. TermCat )
9	5	fucbas	|- ( C Func E ) = ( Base ` ( C FuncCat E ) )
10	1 2	cofucl	|- ( ph -> ( G o.func F ) e. ( C Func E ) )
11	8 9 10 3	termcbasmo	|- ( ph -> ( G o.func F ) = K )