Theorem functermceu

Description: There exists a unique functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025)

	Ref	Expression
Hypotheses	functermceu.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	functermceu.d	No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
Assertion	functermceu	$$⊢\phi \to \exists !ff\in \left(C\mathrm{Func}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		functermceu.c	$$⊢\phi \to C\in \mathrm{Cat}$$
2		functermceu.d	Could not format ( ph -> D e. TermCat ) : No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
3		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}$$
4	3	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}$$
5		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
6		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
7		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
8		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
9		eqid	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_D={\mathrm{Base}}_C\times {\mathrm{Base}}_D$$
10		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)$$
11	1 2 5 6 7 8 9 10	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\}$$
12		sneq	$$⊢f=⟨{\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)⟩\to \left\{f\right\}=\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	12	eqeq2d	$$⊢f=⟨{\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)⟩\to \left(C\mathrm{Func}D=\left\{f\right\}\leftrightarrow 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\}\right)$$
14	4 11 13	spcedv	$$⊢\phi \to \exists fC\mathrm{Func}D=\left\{f\right\}$$
15		eusn	$$⊢\exists !ff\in \left(C\mathrm{Func}D\right)\leftrightarrow \exists fC\mathrm{Func}D=\left\{f\right\}$$
16	14 15	sylibr	$$⊢\phi \to \exists !ff\in \left(C\mathrm{Func}D\right)$$