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 = ( Base ` C )
Assertion	istermc	|- ( C e. TermCat <-> ( C e. ThinCat /\ E. x B = { x } ) )

Proof

Step	Hyp	Ref	Expression
1		istermc.b	|- B = ( Base ` C )
2		fveqeq2	|- ( c = C -> ( ( Base ` c ) = { x } <-> ( Base ` C ) = { x } ) )
3	2	exbidv	|- ( c = C -> ( E. x ( Base ` c ) = { x } <-> E. x ( Base ` C ) = { x } ) )
4	1	eqeq1i	|- ( B = { x } <-> ( Base ` C ) = { x } )
5	4	exbii	|- ( E. x B = { x } <-> E. x ( Base ` C ) = { x } )
6	3 5	bitr4di	|- ( c = C -> ( E. x ( Base ` c ) = { x } <-> E. x B = { x } ) )
7		df-termc	|- TermCat = { c e. ThinCat | E. x ( Base ` c ) = { x } }
8	6 7	elrab2	|- ( C e. TermCat <-> ( C e. ThinCat /\ E. x B = { x } ) )