Metamath Proof Explorer

Theorem termcthin

Description: A terminal category is a thin category. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Assertion termcthin 
|- ( C e. TermCat -> C e. ThinCat )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` C ) = ( Base ` C )
2 1 istermc 
 |-  ( C e. TermCat <-> ( C e. ThinCat /\ E. x ( Base ` C ) = { x } ) )
3 2 simplbi 
 |-  ( C e. TermCat -> C e. ThinCat )