Metamath Proof Explorer

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 ∈ ZeroO ⁡ C → O ∈ B

Proof

Step Hyp Ref Expression
1 initoo2.b ⊢ B = Base C
2 zeroorcl ⊢ O ∈ ZeroO ⁡ C → C ∈ Cat
3 iszeroi ⊢ C ∈ Cat ∧ O ∈ ZeroO ⁡ C → O ∈ Base C ∧ O ∈ InitO ⁡ C ∧ O ∈ TermO ⁡ C
4 3 simpld ⊢ C ∈ Cat ∧ O ∈ ZeroO ⁡ C → O ∈ Base C
5 2 4 mpancom ⊢ O ∈ ZeroO ⁡ C → O ∈ Base C
6 5 1 eleqtrrdi ⊢ O ∈ ZeroO ⁡ C → O ∈ B