Theorem thincc

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

	Ref	Expression
Assertion	thincc	Could not format assertion : No typesetting found for |- ( C e. ThinCat -> C e. Cat ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
2		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
3	1 2	isthinc	Could not format ( C e. ThinCat <-> ( C e. Cat /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) ) : No typesetting found for |- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) ) with typecode |-
4	3	simplbi	Could not format ( C e. ThinCat -> C e. Cat ) : No typesetting found for |- ( C e. ThinCat -> C e. Cat ) with typecode |-