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

Metamath Proof Explorer

Theorem setc1obas

Description: The base of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025)

Ref Expression
Hypothesis funcsetc1o.1 ⊢ 1 = ( SetCat ‘ 1o )
Assertion setc1obas 1o = ( Base ‘ 1 )

Proof

Step Hyp Ref Expression
1 funcsetc1o.1 ⊢ 1 = ( SetCat ‘ 1o )
2 1oex ⊢ 1o ∈ V
3 2 a1i ⊢ ( ⊤ → 1o ∈ V )
4 1 3 setcbas ⊢ ( ⊤ → 1o = ( Base ‘ 1 ) )
5 4 mptru ⊢ 1o = ( Base ‘ 1 )