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

Metamath Proof Explorer

Theorem setcsnterm

Description: The category of one set, either a singleton set or an empty set, is terminal. (Contributed by Zhi Wang, 18-Oct-2025)

Ref Expression
Assertion setcsnterm 
|- ( SetCat ` { { A } } ) e. TermCat

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( T. -> ( SetCat ` { { A } } ) = ( SetCat ` { { A } } ) )
2 snex 
 |-  { { A } } e. _V
3 2 a1i 
 |-  ( T. -> { { A } } e. _V )
4 velsn 
 |-  ( x e. { { A } } <-> x = { A } )
5 mosn 
 |-  ( x = { A } -> E* p p e. x )
6 4 5 sylbi 
 |-  ( x e. { { A } } -> E* p p e. x )
7 6 rgen 
 |-  A. x e. { { A } } E* p p e. x
8 7 a1i 
 |-  ( T. -> A. x e. { { A } } E* p p e. x )
9 1 3 8 setcthin 
 |-  ( T. -> ( SetCat ` { { A } } ) e. ThinCat )
10 9 mptru 
 |-  ( SetCat ` { { A } } ) e. ThinCat
11 snex 
 |-  { A } e. _V
12 11 ensn1 
 |-  { { A } } ~~ 1o
13 eqid 
 |-  ( SetCat ` { { A } } ) = ( SetCat ` { { A } } )
14 13 3 setcbas 
 |-  ( T. -> { { A } } = ( Base ` ( SetCat ` { { A } } ) ) )
15 14 mptru 
 |-  { { A } } = ( Base ` ( SetCat ` { { A } } ) )
16 15 istermc3 
 |-  ( ( SetCat ` { { A } } ) e. TermCat <-> ( ( SetCat ` { { A } } ) e. ThinCat /\ { { A } } ~~ 1o ) )
17 10 12 16 mpbir2an 
 |-  ( SetCat ` { { A } } ) e. TermCat