Theorem thincssc

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

	Ref	Expression
Assertion	thincssc	$$⊢\mathrm{ThinCat}\subseteq \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		thincc	$$⊢c\in \mathrm{ThinCat}\to c\in \mathrm{Cat}$$
2	1	ssriv	$$⊢\mathrm{ThinCat}\subseteq \mathrm{Cat}$$