Theorem termoo2

Description: A terminal object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025)

	Ref	Expression
Hypothesis	initoo2.b	|- B = ( Base ` C )
Assertion	termoo2	|- ( O e. ( TermO ` C ) -> O e. B )

Proof

Step	Hyp	Ref	Expression
1		initoo2.b	|- B = ( Base ` C )
2		eqid	|- ( Hom ` C ) = ( Hom ` C )
3		termorcl	|- ( O e. ( TermO ` C ) -> C e. Cat )
4	1 2 3	istermoi	|- ( ( O e. ( TermO ` C ) /\ O e. ( TermO ` C ) ) -> ( O e. B /\ A. b e. B E! h h e. ( b ( Hom ` C ) O ) ) )
5	4	anidms	|- ( O e. ( TermO ` C ) -> ( O e. B /\ A. b e. B E! h h e. ( b ( Hom ` C ) O ) ) )
6	5	simpld	|- ( O e. ( TermO ` C ) -> O e. B )