Theorem thincssc

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

	Ref	Expression
Assertion	thincssc	⊢ ThinCat ⊆ Cat

Proof

Step	Hyp	Ref	Expression
1		thincc	⊢ ( 𝑐 ∈ ThinCat → 𝑐 ∈ Cat )
2	1	ssriv	⊢ ThinCat ⊆ Cat