Theorem discbas

Description: A discrete category (a category whose only morphisms are the identity morphisms) can be constructed for any base set. (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	discbas	$$⊢B\in V\to B={\mathrm{Base}}_C$$

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	1	resiposbas	$$⊢B\in V\to B={\mathrm{Base}}_K$$
8	3 6 7	prstcbas	$$⊢B\in V\to B={\mathrm{Base}}_C$$