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

Metamath Proof Explorer

Theorem discsnterm

Description: A discrete category (a category whose only morphisms are the identity morphisms) with a singlegon base is terminal. Corollary of example 3.3(4)(c) of Adamek p. 24 and example 3.26(1) of Adamek p. 33. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypotheses discthin.k 
|- K = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. }
discthin.c 
|- C = ( ProsetToCat ` K )
Assertion discsnterm 
|- ( E. x B = { x } -> C e. TermCat )

Proof

Step Hyp Ref Expression
1 discthin.k 
 |-  K = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. }
2 discthin.c 
 |-  C = ( ProsetToCat ` K )
3 discsntermlem 
 |-  ( E. x B = { x } -> B e. { b | E. x b = { x } } )
4 1 2 discthin 
 |-  ( B e. { b | E. x b = { x } } -> C e. ThinCat )
5 3 4 syl 
 |-  ( E. x B = { x } -> C e. ThinCat )
6 elex 
 |-  ( B e. { b | E. x b = { x } } -> B e. _V )
7 1 2 discbas 
 |-  ( B e. _V -> B = ( Base ` C ) )
8 7 eqeq1d 
 |-  ( B e. _V -> ( B = { x } <-> ( Base ` C ) = { x } ) )
9 8 exbidv 
 |-  ( B e. _V -> ( E. x B = { x } <-> E. x ( Base ` C ) = { x } ) )
10 3 6 9 3syl 
 |-  ( E. x B = { x } -> ( E. x B = { x } <-> E. x ( Base ` C ) = { x } ) )
11 10 ibi 
 |-  ( E. x B = { x } -> E. x ( Base ` C ) = { x } )
12 eqid 
 |-  ( Base ` C ) = ( Base ` C )
13 12 istermc 
 |-  ( C e. TermCat <-> ( C e. ThinCat /\ E. x ( Base ` C ) = { x } ) )
14 5 11 13 sylanbrc 
 |-  ( E. x B = { x } -> C e. TermCat )