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	Could not format assertion : No typesetting found for |- ( SetCat ` { { A } } ) e. TermCat with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqidd	$$⊢\top \to \mathrm{SetCat}\left(\left\{\left\{A\right\}\right\}\right)=\mathrm{SetCat}\left(\left\{\left\{A\right\}\right\}\right)$$
2		snex	$$⊢\left\{\left\{A\right\}\right\}\in \mathrm{V}$$
3	2	a1i	$$⊢\top \to \left\{\left\{A\right\}\right\}\in \mathrm{V}$$
4		velsn	$$⊢x\in \left\{\left\{A\right\}\right\}\leftrightarrow x=\left\{A\right\}$$
5		mosn	$$⊢x=\left\{A\right\}\to {\exists }^{*}pp\in x$$
6	4 5	sylbi	$$⊢x\in \left\{\left\{A\right\}\right\}\to {\exists }^{*}pp\in x$$
7	6	rgen	$$⊢\forall x\in \left\{\left\{A\right\}\right\}{\exists }^{*}pp\in x$$
8	7	a1i	$$⊢\top \to \forall x\in \left\{\left\{A\right\}\right\}{\exists }^{*}pp\in x$$
9	1 3 8	setcthin	$$⊢\top \to \mathrm{SetCat}\left(\left\{\left\{A\right\}\right\}\right)\in \mathrm{ThinCat}$$
10	9	mptru	$$⊢\mathrm{SetCat}\left(\left\{\left\{A\right\}\right\}\right)\in \mathrm{ThinCat}$$
11		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
12	11	ensn1	$$⊢\left\{\left\{A\right\}\right\}\approx 1_{𝑜}$$
13		eqid	$$⊢\mathrm{SetCat}\left(\left\{\left\{A\right\}\right\}\right)=\mathrm{SetCat}\left(\left\{\left\{A\right\}\right\}\right)$$
14	13 3	setcbas	$$⊢\top \to \left\{\left\{A\right\}\right\}={\mathrm{Base}}_{\mathrm{SetCat}\left(\left\{\left\{A\right\}\right\}\right)}$$
15	14	mptru	$$⊢\left\{\left\{A\right\}\right\}={\mathrm{Base}}_{\mathrm{SetCat}\left(\left\{\left\{A\right\}\right\}\right)}$$
16	15	istermc3	Could not format ( ( SetCat ` { { A } } ) e. TermCat <-> ( ( SetCat ` { { A } } ) e. ThinCat /\ { { A } } ~~ 1o ) ) : No typesetting found for |- ( ( SetCat ` { { A } } ) e. TermCat <-> ( ( SetCat ` { { A } } ) e. ThinCat /\ { { A } } ~~ 1o ) ) with typecode |-
17	10 12 16	mpbir2an	Could not format ( SetCat ` { { A } } ) e. TermCat : No typesetting found for |- ( SetCat ` { { A } } ) e. TermCat with typecode |-