Theorem termoo

Description: A terminal object is an object. (Contributed by AV, 18-Apr-2020)

	Ref	Expression
Assertion	termoo	|- ( C e. Cat -> ( O e. ( TermO ` 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	istermoi	|- ( ( C e. Cat /\ O e. ( TermO ` C ) ) -> ( O e. ( Base ` C ) /\ A. b e. ( Base ` C ) E! h h e. ( b ( Hom ` C ) O ) ) )
5	4	simpld	|- ( ( C e. Cat /\ O e. ( TermO ` C ) ) -> O e. ( Base ` C ) )
6	5	ex	|- ( C e. Cat -> ( O e. ( TermO ` C ) -> O e. ( Base ` C ) ) )