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	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	zeroo2	⊢ ( 𝑂 ∈ ( ZeroO ‘ 𝐶 ) → 𝑂 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		initoo2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		zeroorcl	⊢ ( 𝑂 ∈ ( ZeroO ‘ 𝐶 ) → 𝐶 ∈ Cat )
3		iszeroi	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( ZeroO ‘ 𝐶 ) ) → ( 𝑂 ∈ ( Base ‘ 𝐶 ) ∧ ( 𝑂 ∈ ( InitO ‘ 𝐶 ) ∧ 𝑂 ∈ ( TermO ‘ 𝐶 ) ) ) )
4	3	simpld	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( ZeroO ‘ 𝐶 ) ) → 𝑂 ∈ ( Base ‘ 𝐶 ) )
5	2 4	mpancom	⊢ ( 𝑂 ∈ ( ZeroO ‘ 𝐶 ) → 𝑂 ∈ ( Base ‘ 𝐶 ) )
6	5 1	eleqtrrdi	⊢ ( 𝑂 ∈ ( ZeroO ‘ 𝐶 ) → 𝑂 ∈ 𝐵 )