Theorem initoo

Description: An initial object is an object. (Contributed by AV, 14-Apr-2020)

	Ref	Expression
Assertion	initoo	|- ( C e. Cat -> ( O e. ( InitO ` C ) -> O e. ( Base ` C ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` C ) = ( Base ` C )
2		eqid	|- ( Hom ` C ) = ( Hom ` C )
3		id	|- ( C e. Cat -> C e. Cat )
4	1 2 3	isinitoi	|- ( ( C e. Cat /\ O e. ( InitO ` C ) ) -> ( O e. ( Base ` C ) /\ A. b e. ( Base ` C ) E! h h e. ( O ( Hom ` C ) b ) ) )
5	4	simpld	|- ( ( C e. Cat /\ O e. ( InitO ` C ) ) -> O e. ( Base ` C ) )
6	5	ex	|- ( C e. Cat -> ( O e. ( InitO ` C ) -> O e. ( Base ` C ) ) )