This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem thincssc

Description: A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Assertion thincssc 
|- ThinCat C_ Cat

Proof

Step Hyp Ref Expression
1 thincc 
 |-  ( c e. ThinCat -> c e. Cat )
2 1 ssriv 
 |-  ThinCat C_ Cat