This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) )