Metamath Proof Explorer


Theorem termoo

Description: A terminal object is an object. (Contributed by AV, 18-Apr-2020)

Ref Expression
Assertion termoo CCatOTermOCOBaseC

Proof

Step Hyp Ref Expression
1 eqid BaseC=BaseC
2 eqid HomC=HomC
3 id CCatCCat
4 1 2 3 istermoi CCatOTermOCOBaseCbBaseC∃!hhbHomCO
5 4 simpld CCatOTermOCOBaseC
6 5 ex CCatOTermOCOBaseC