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

Metamath Proof Explorer

Theorem setc1oid

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

Step	Hyp	Ref	Expression
1		funcsetc1o.1	$⊢ \underset{˙}{1} = SetCat (1_{𝑜})$
2		setc1oid.i	$⊢ I = Id (\underset{˙}{1})$
3		1oex	$⊢ 1_{𝑜} \in V$
4	3	a1i	$⊢ ⊤ \to 1_{𝑜} \in V$
5		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
6	5	a1i	$⊢ ⊤ \to \emptyset \in 1_{𝑜}$
7	1 2 4 6	setcid	$⊢ ⊤ \to I (\emptyset) = {I ↾}_{\emptyset}$
8	7	mptru	$⊢ I (\emptyset) = {I ↾}_{\emptyset}$
9		res0	$⊢ {I ↾}_{\emptyset} = \emptyset$
10	8 9	eqtri	$⊢ I (\emptyset) = \emptyset$