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 \|-

Step	Hyp	Ref	Expression
1		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
2		vsn	$⊢ \{V\} = \emptyset$
3	2	sneqi	$⊢ \{\{V\}\} = \{\emptyset\}$
4	1 3	eqtr4i	$⊢ 1_{𝑜} = \{\{V\}\}$
5	4	fveq2i	$⊢ SetCat (1_{𝑜}) = SetCat (\{\{V\}\})$
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 \|-

Metamath Proof Explorer