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 e. _V
3 2 a1i 
 |-  ( T. -> 1o e. _V )
4 1 3 setcbas 
 |-  ( T. -> 1o = ( Base ` .1. ) )
5 4 mptru 
 |-  1o = ( Base ` .1. )