Metamath Proof Explorer

Theorem zeroorcl

Description: Reverse closure for a zero object: If a class has a zero object, the class is a category. (Contributed by AV, 4-Apr-2020)

Ref Expression
Assertion zeroorcl ⊢ Z ∈ ZeroO ⁡ C → C ∈ Cat

Proof

Step Hyp Ref Expression
1 df-zeroo ⊢ ZeroO = c ∈ Cat ⟼ InitO ⁡ c ∩ TermO ⁡ c
2 1 mptrcl ⊢ Z ∈ ZeroO ⁡ C → C ∈ Cat