Theorem istermc2

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

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

Proof

Step	Hyp	Ref	Expression
1		istermc.b	$$⊢B={\mathrm{Base}}_C$$
2	1	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 |-
3		eusn	$$⊢\exists !xx\in B\leftrightarrow \exists xB=\left\{x\right\}$$
4	3	anbi2i	$$⊢\left(C\in \mathrm{ThinCat}\wedge \exists !xx\in B\right)\leftrightarrow \left(C\in \mathrm{ThinCat}\wedge \exists xB=\left\{x\right\}\right)$$
5	2 4	bitr4i	Could not format ( C e. TermCat <-> ( C e. ThinCat /\ E! x x e. B ) ) : No typesetting found for |- ( C e. TermCat <-> ( C e. ThinCat /\ E! x x e. B ) ) with typecode |-