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 e. ( TermO ` C ) -> C e. Cat )

Proof

Step	Hyp	Ref	Expression
1		df-termo	|- TermO = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } )
2	1	mptrcl	|- ( T e. ( TermO ` C ) -> C e. Cat )