Theorem termorcl

Description: Reverse closure for a terminal object: If a class has a terminal object, the class is a category. (Contributed by AV, 4-Apr-2020)

	Ref	Expression
Assertion	termorcl	$$⊢T\in \mathrm{TermO}\left(C\right)\to C\in \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2	1	mptrcl	$$⊢T\in \mathrm{TermO}\left(C\right)\to C\in \mathrm{Cat}$$