Metamath Proof Explorer

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 ) e. 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 } } ) e. TermCat
7 5 6 eqeltri 
 |-  ( SetCat ` 1o ) e. TermCat