Theorem termcbas

Description: The base of a terminal category is a singleton. (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypotheses	termcbas.c	No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
	termcbas.b	$$⊢B={\mathrm{Base}}_C$$
Assertion	termcbas	$$⊢\phi \to \exists xB=\left\{x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		termcbas.c	Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
2		termcbas.b	$$⊢B={\mathrm{Base}}_C$$
3	2	istermc	Could not format ( C e. TermCat <-> ( C e. ThinCat /\ E. x B = { x } ) ) : No typesetting found for |- ( C e. TermCat <-> ( C e. ThinCat /\ E. x B = { x } ) ) with typecode |-
4	1 3	sylib	$$⊢\phi \to \left(C\in \mathrm{ThinCat}\wedge \exists xB=\left\{x\right\}\right)$$
5	4	simprd	$$⊢\phi \to \exists xB=\left\{x\right\}$$