Theorem discthin

Description: A discrete category (a category whose only morphisms are the identity morphisms) is thin. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Hypotheses	discthin.k	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_B⟩\right\}$$
	discthin.c	$$⊢C=\mathrm{ProsetToCat}\left(K\right)$$
Assertion	discthin	$$⊢B\in V\to C\in \mathrm{ThinCat}$$

Proof

Step	Hyp	Ref	Expression
1		discthin.k	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_B⟩\right\}$$
2		discthin.c	$$⊢C=\mathrm{ProsetToCat}\left(K\right)$$
3	2	a1i	$$⊢B\in V\to C=\mathrm{ProsetToCat}\left(K\right)$$
4	1	resipos	$$⊢B\in V\to K\in \mathrm{Poset}$$
5		posprs	$$⊢K\in \mathrm{Poset}\to K\in \mathrm{Proset}$$
6	4 5	syl	$$⊢B\in V\to K\in \mathrm{Proset}$$
7	3 6	prstcthin	$$⊢B\in V\to C\in \mathrm{ThinCat}$$