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 = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. }
	discthin.c	|- C = ( ProsetToCat ` K )
Assertion	discbas	|- ( B e. V -> B = ( Base ` C ) )

Proof

Step	Hyp	Ref	Expression
1		discthin.k	|- K = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. }
2		discthin.c	|- C = ( ProsetToCat ` K )
3	2	a1i	|- ( B e. V -> C = ( ProsetToCat ` K ) )
4	1	resipos	|- ( B e. V -> K e. Poset )
5		posprs	|- ( K e. Poset -> K e. Proset )
6	4 5	syl	|- ( B e. V -> K e. Proset )
7	1	resiposbas	|- ( B e. V -> B = ( Base ` K ) )
8	3 6 7	prstcbas	|- ( B e. V -> B = ( Base ` C ) )