Theorem fucterm

Description: The category of functors to a terminal category is terminal. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	funcsn.q	$$⊢Q=C\mathrm{FuncCat}D$$
	fucterm.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	fucterm.d	No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
Assertion	fucterm	Could not format assertion : No typesetting found for |- ( ph -> Q e. TermCat ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		funcsn.q	$$⊢Q=C\mathrm{FuncCat}D$$
2		fucterm.c	$$⊢\phi \to C\in \mathrm{Cat}$$
3		fucterm.d	Could not format ( ph -> D e. TermCat ) : No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
4		opex	$$⊢⟨{\mathrm{Base}}_C\times {\mathrm{Base}}_D,\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Hom}\left(C\right)y\right)\times \left(\left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\left(x\right)\mathrm{Hom}\left(D\right)\left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\left(y\right)\right)\right)⟩\in \mathrm{V}$$
5	4	a1i	$$⊢\phi \to ⟨{\mathrm{Base}}_C\times {\mathrm{Base}}_D,\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Hom}\left(C\right)y\right)\times \left(\left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\left(x\right)\mathrm{Hom}\left(D\right)\left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\left(y\right)\right)\right)⟩\in \mathrm{V}$$
6		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
7		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
8		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
9		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
10		eqid	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_D={\mathrm{Base}}_C\times {\mathrm{Base}}_D$$
11		eqid	$$⊢\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Hom}\left(C\right)y\right)\times \left(\left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\left(x\right)\mathrm{Hom}\left(D\right)\left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\left(y\right)\right)\right)=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Hom}\left(C\right)y\right)\times \left(\left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\left(x\right)\mathrm{Hom}\left(D\right)\left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\left(y\right)\right)\right)$$
12	2 3 6 7 8 9 10 11	functermc2	$$⊢\phi \to C\mathrm{Func}D=\left\{⟨{\mathrm{Base}}_C\times {\mathrm{Base}}_D,\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Hom}\left(C\right)y\right)\times \left(\left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\left(x\right)\mathrm{Hom}\left(D\right)\left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\left(y\right)\right)\right)⟩\right\}$$
13	3	termcthind	$$⊢\phi \to D\in \mathrm{ThinCat}$$
14	1 5 12 13	funcsn	Could not format ( ph -> Q e. TermCat ) : No typesetting found for |- ( ph -> Q e. TermCat ) with typecode |-