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 )