Theorem discsnterm

Description: A discrete category (a category whose only morphisms are the identity morphisms) with a singlegon base is terminal. (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	discsnterm	|- ( E. x B = { x } -> C e. TermCat )

Proof

Step	Hyp	Ref	Expression
1		discthin.k	|- K = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. }
2		discthin.c	|- C = ( ProsetToCat ` K )
3		discsntermlem	|- ( E. x B = { x } -> B e. { b | E. x b = { x } } )
4	1 2	discthin	|- ( B e. { b | E. x b = { x } } -> C e. ThinCat )
5	3 4	syl	|- ( E. x B = { x } -> C e. ThinCat )
6		elex	|- ( B e. { b | E. x b = { x } } -> B e. _V )
7	1 2	discbas	|- ( B e. _V -> B = ( Base ` C ) )
8	7	eqeq1d	|- ( B e. _V -> ( B = { x } <-> ( Base ` C ) = { x } ) )
9	8	exbidv	|- ( B e. _V -> ( E. x B = { x } <-> E. x ( Base ` C ) = { x } ) )
10	3 6 9	3syl	|- ( E. x B = { x } -> ( E. x B = { x } <-> E. x ( Base ` C ) = { x } ) )
11	10	ibi	|- ( E. x B = { x } -> E. x ( Base ` C ) = { x } )
12		eqid	|- ( Base ` C ) = ( Base ` C )
13	12	istermc	|- ( C e. TermCat <-> ( C e. ThinCat /\ E. x ( Base ` C ) = { x } ) )
14	5 11 13	sylanbrc	|- ( E. x B = { x } -> C e. TermCat )