Theorem zeroo2

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

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

Proof

Step	Hyp	Ref	Expression
1		initoo2.b	|- B = ( Base ` C )
2		zeroorcl	|- ( O e. ( ZeroO ` C ) -> C e. Cat )
3		iszeroi	|- ( ( C e. Cat /\ O e. ( ZeroO ` C ) ) -> ( O e. ( Base ` C ) /\ ( O e. ( InitO ` C ) /\ O e. ( TermO ` C ) ) ) )
4	3	simpld	|- ( ( C e. Cat /\ O e. ( ZeroO ` C ) ) -> O e. ( Base ` C ) )
5	2 4	mpancom	|- ( O e. ( ZeroO ` C ) -> O e. ( Base ` C ) )
6	5 1	eleqtrrdi	|- ( O e. ( ZeroO ` C ) -> O e. B )