Theorem cofuterm

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

	Ref	Expression
Hypotheses	cofuterm.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	cofuterm.g	$$⊢\phi \to G\in \left(D\mathrm{Func}E\right)$$
	cofuterm.k	$$⊢\phi \to K\in \left(C\mathrm{Func}E\right)$$
	cofuterm.e	No typesetting found for |- ( ph -> E e. TermCat ) with typecode |-
Assertion	cofuterm	$$⊢\phi \to G{\circ }_{\mathrm{func}}F=K$$

Proof

Step	Hyp	Ref	Expression
1		cofuterm.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
2		cofuterm.g	$$⊢\phi \to G\in \left(D\mathrm{Func}E\right)$$
3		cofuterm.k	$$⊢\phi \to K\in \left(C\mathrm{Func}E\right)$$
4		cofuterm.e	Could not format ( ph -> E e. TermCat ) : No typesetting found for |- ( ph -> E e. TermCat ) with typecode |-
5		eqid	$$⊢C\mathrm{FuncCat}E=C\mathrm{FuncCat}E$$
6	1	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
7	6	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
8	5 7 4	fucterm	Could not format ( ph -> ( C FuncCat E ) e. TermCat ) : No typesetting found for |- ( ph -> ( C FuncCat E ) e. TermCat ) with typecode |-
9	5	fucbas	$$⊢C\mathrm{Func}E={\mathrm{Base}}_{\left(C\mathrm{FuncCat}E\right)}$$
10	1 2	cofucl	$$⊢\phi \to G{\circ }_{\mathrm{func}}F\in \left(C\mathrm{Func}E\right)$$
11	8 9 10 3	termcbasmo	$$⊢\phi \to G{\circ }_{\mathrm{func}}F=K$$