Theorem istermc

Description: The predicate "is a terminal category". A terminal category is a thin category with a singleton base set. (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypothesis	istermc.b	$$⊢B={\mathrm{Base}}_C$$
Assertion	istermc	Could not format assertion : No typesetting found for |- ( C e. TermCat <-> ( C e. ThinCat /\ E. x B = { x } ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		istermc.b	$$⊢B={\mathrm{Base}}_C$$
2		fveqeq2	$$⊢c=C\to \left({\mathrm{Base}}_c=\left\{x\right\}\leftrightarrow {\mathrm{Base}}_C=\left\{x\right\}\right)$$
3	2	exbidv	$$⊢c=C\to \left(\exists x{\mathrm{Base}}_c=\left\{x\right\}\leftrightarrow \exists x{\mathrm{Base}}_C=\left\{x\right\}\right)$$
4	1	eqeq1i	$$⊢B=\left\{x\right\}\leftrightarrow {\mathrm{Base}}_C=\left\{x\right\}$$
5	4	exbii	$$⊢\exists xB=\left\{x\right\}\leftrightarrow \exists x{\mathrm{Base}}_C=\left\{x\right\}$$
6	3 5	bitr4di	$$⊢c=C\to \left(\exists x{\mathrm{Base}}_c=\left\{x\right\}\leftrightarrow \exists xB=\left\{x\right\}\right)$$
7		df-termc	Could not format TermCat = { c e. ThinCat | E. x ( Base ` c ) = { x } } : No typesetting found for |- TermCat = { c e. ThinCat | E. x ( Base ` c ) = { x } } with typecode |-
8	6 7	elrab2	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 |-