Theorem setc1oterm

Description: The category ( SetCat1o ) , i.e., thetrivial category, is terminal. (Contributed by Zhi Wang, 18-Oct-2025)

	Ref	Expression
Assertion	setc1oterm	Could not format assertion : No typesetting found for |- ( SetCat ` 1o ) e. TermCat with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
2		vsn	$$⊢\left\{\mathrm{V}\right\}=\varnothing$$
3	2	sneqi	$$⊢\left\{\left\{\mathrm{V}\right\}\right\}=\left\{\varnothing \right\}$$
4	1 3	eqtr4i	$$⊢1_{𝑜}=\left\{\left\{\mathrm{V}\right\}\right\}$$
5	4	fveq2i	$$⊢\mathrm{SetCat}\left(1_{𝑜}\right)=\mathrm{SetCat}\left(\left\{\left\{\mathrm{V}\right\}\right\}\right)$$
6		setcsnterm	Could not format ( SetCat ` { { _V } } ) e. TermCat : No typesetting found for |- ( SetCat ` { { _V } } ) e. TermCat with typecode |-
7	5 6	eqeltri	Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for |- ( SetCat ` 1o ) e. TermCat with typecode |-