Theorem termcthin

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

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

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
2	1	istermc	Could not format ( C e. TermCat <-> ( C e. ThinCat /\ E. x ( Base ` C ) = { x } ) ) : No typesetting found for |- ( C e. TermCat <-> ( C e. ThinCat /\ E. x ( Base ` C ) = { x } ) ) with typecode |-
3	2	simplbi	Could not format ( C e. TermCat -> C e. ThinCat ) : No typesetting found for |- ( C e. TermCat -> C e. ThinCat ) with typecode |-