Metamath Proof Explorer

Theorem termccd

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

Ref Expression
Hypothesis termcthind.c 
|- ( ph -> C e. TermCat )
Assertion termccd 
|- ( ph -> C e. Cat )

Proof

Step Hyp Ref Expression
1 termcthind.c 
 |-  ( ph -> C e. TermCat )
2 1 termcthind 
 |-  ( ph -> C e. ThinCat )
3 2 thinccd 
 |-  ( ph -> C e. Cat )