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 e. ( ZeroO ` C ) -> C e. Cat )

Proof

Step Hyp Ref Expression
1 df-zeroo 
 |-  ZeroO = ( c e. Cat |-> ( ( InitO ` c ) i^i ( TermO ` c ) ) )
2 1 mptrcl 
 |-  ( Z e. ( ZeroO ` C ) -> C e. Cat )