Theorem discsnterm

Description: A discrete category (a category whose only morphisms are the identity morphisms) with a singlegon base is terminal. Corollary of example 3.3(4)(c) of Adamek p. 24 and example 3.26(1) of Adamek p. 33. (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	discsnterm	Could not format assertion : No typesetting found for |- ( E. x B = { x } -> C e. TermCat ) with typecode |-

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		discsntermlem	$$⊢\exists xB=\left\{x\right\}\to B\in \left\{b|\exists xb=\left\{x\right\}\right\}$$
4	1 2	discthin	$$⊢B\in \left\{b|\exists xb=\left\{x\right\}\right\}\to C\in \mathrm{ThinCat}$$
5	3 4	syl	$$⊢\exists xB=\left\{x\right\}\to C\in \mathrm{ThinCat}$$
6		elex	$$⊢B\in \left\{b|\exists xb=\left\{x\right\}\right\}\to B\in \mathrm{V}$$
7	1 2	discbas	$$⊢B\in \mathrm{V}\to B={\mathrm{Base}}_C$$
8	7	eqeq1d	$$⊢B\in \mathrm{V}\to \left(B=\left\{x\right\}\leftrightarrow {\mathrm{Base}}_C=\left\{x\right\}\right)$$
9	8	exbidv	$$⊢B\in \mathrm{V}\to \left(\exists xB=\left\{x\right\}\leftrightarrow \exists x{\mathrm{Base}}_C=\left\{x\right\}\right)$$
10	3 6 9	3syl	$$⊢\exists xB=\left\{x\right\}\to \left(\exists xB=\left\{x\right\}\leftrightarrow \exists x{\mathrm{Base}}_C=\left\{x\right\}\right)$$
11	10	ibi	$$⊢\exists xB=\left\{x\right\}\to \exists x{\mathrm{Base}}_C=\left\{x\right\}$$
12		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
13	12	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 |-
14	5 11 13	sylanbrc	Could not format ( E. x B = { x } -> C e. TermCat ) : No typesetting found for |- ( E. x B = { x } -> C e. TermCat ) with typecode |-