Theorem setc1oterm

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

	Ref	Expression
Assertion	setc1oterm	⊢ ( SetCat ‘ 1o ) ∈ TermCat

Proof

Step	Hyp	Ref	Expression
1		df1o2	⊢ 1o = { ∅ }
2		vsn	⊢ { V } = ∅
3	2	sneqi	⊢ { { V } } = { ∅ }
4	1 3	eqtr4i	⊢ 1o = { { V } }
5	4	fveq2i	⊢ ( SetCat ‘ 1o ) = ( SetCat ‘ { { V } } )
6		setcsnterm	⊢ ( SetCat ‘ { { V } } ) ∈ TermCat
7	5 6	eqeltri	⊢ ( SetCat ‘ 1o ) ∈ TermCat