Metamath Proof Explorer


Theorem termorcl

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

Ref Expression
Assertion termorcl TTermOCCCat

Proof

Step Hyp Ref Expression
1 df-termo TermO=cCataBasec|bBasec∃!hhbHomca
2 1 mptrcl TTermOCCCat