Theorem termofn

Description: TermO is a function on Cat . (Contributed by Zhi Wang, 29-Aug-2024)

	Ref	Expression
Assertion	termofn	$$⊢\mathrm{TermO}Fn\mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢{\mathrm{Base}}_c\in \mathrm{V}$$
2	1	rabex	$$⊢\left\{a\in {\mathrm{Base}}_c|\forall b\in {\mathrm{Base}}_c\exists !hh\in \left(b\mathrm{Hom}\left(c\right)a\right)\right\}\in \mathrm{V}$$
3		df-termo	$$⊢\mathrm{TermO}=\left(c\in \mathrm{Cat}⟼\left\{a\in {\mathrm{Base}}_c|\forall b\in {\mathrm{Base}}_c\exists !hh\in \left(b\mathrm{Hom}\left(c\right)a\right)\right\}\right)$$
4	2 3	fnmpti	$$⊢\mathrm{TermO}Fn\mathrm{Cat}$$