Theorem setc1oid

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

	Ref	Expression
Hypotheses	funcsetc1o.1	⊢ 1 = ( SetCat ‘ 1o )
	setc1oid.i	⊢ 𝐼 = ( Id ‘ 1 )
Assertion	setc1oid	⊢ ( 𝐼 ‘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		funcsetc1o.1	⊢ 1 = ( SetCat ‘ 1o )
2		setc1oid.i	⊢ 𝐼 = ( Id ‘ 1 )
3		1oex	⊢ 1o ∈ V
4	3	a1i	⊢ ( ⊤ → 1o ∈ V )
5		0lt1o	⊢ ∅ ∈ 1o
6	5	a1i	⊢ ( ⊤ → ∅ ∈ 1o )
7	1 2 4 6	setcid	⊢ ( ⊤ → ( 𝐼 ‘ ∅ ) = ( I ↾ ∅ ) )
8	7	mptru	⊢ ( 𝐼 ‘ ∅ ) = ( I ↾ ∅ )
9		res0	⊢ ( I ↾ ∅ ) = ∅
10	8 9	eqtri	⊢ ( 𝐼 ‘ ∅ ) = ∅