Theorem istermc3

Description: The predicate "is a terminal category". A terminal category is a thin category whose base set is equinumerous to 1o . Consider en1b , map1 , and euen1b . (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypothesis	istermc.b	|- B = ( Base ` C )
Assertion	istermc3	|- ( C e. TermCat <-> ( C e. ThinCat /\ B ~~ 1o ) )

Proof

Step	Hyp	Ref	Expression
1		istermc.b	|- B = ( Base ` C )
2	1	istermc	|- ( C e. TermCat <-> ( C e. ThinCat /\ E. x B = { x } ) )
3		en1	|- ( B ~~ 1o <-> E. x B = { x } )
4	3	anbi2i	|- ( ( C e. ThinCat /\ B ~~ 1o ) <-> ( C e. ThinCat /\ E. x B = { x } ) )
5	2 4	bitr4i	|- ( C e. TermCat <-> ( C e. ThinCat /\ B ~~ 1o ) )