Theorem initorcl

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

	Ref	Expression
Assertion	initorcl	|- ( I e. ( InitO ` C ) -> C e. Cat )

Proof

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