Theorem setc1oid

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

	Ref	Expression
Hypotheses	funcsetc1o.1	$$⊢\underset{\dot{}}{1}=\mathrm{SetCat}\left(1_{𝑜}\right)$$
	setc1oid.i	$$⊢I=\mathrm{Id}\left(\underset{\dot{}}{1}\right)$$
Assertion	setc1oid	$$⊢I\left(\varnothing \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		funcsetc1o.1	$$⊢\underset{\dot{}}{1}=\mathrm{SetCat}\left(1_{𝑜}\right)$$
2		setc1oid.i	$$⊢I=\mathrm{Id}\left(\underset{\dot{}}{1}\right)$$
3		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
4	3	a1i	$$⊢\top \to 1_{𝑜}\in \mathrm{V}$$
5		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
6	5	a1i	$$⊢\top \to \varnothing \in 1_{𝑜}$$
7	1 2 4 6	setcid	$$⊢\top \to I\left(\varnothing \right)={\mathrm{I}\upharpoonright }_{\varnothing }$$
8	7	mptru	$$⊢I\left(\varnothing \right)={\mathrm{I}\upharpoonright }_{\varnothing }$$
9		res0	$$⊢{\mathrm{I}\upharpoonright }_{\varnothing }=\varnothing$$
10	8 9	eqtri	$$⊢I\left(\varnothing \right)=\varnothing$$