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