This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ∈ 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