Theorem setc1ohomfval

Description: Set of morphisms of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025)

	Ref	Expression
Hypothesis	funcsetc1o.1	$$⊢\underset{\dot{}}{1}=\mathrm{SetCat}\left(1_{𝑜}\right)$$
Assertion	setc1ohomfval	$$⊢\left\{⟨\varnothing ,\varnothing ,1_{𝑜}⟩\right\}=\mathrm{Hom}\left(\underset{\dot{}}{1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		funcsetc1o.1	$$⊢\underset{\dot{}}{1}=\mathrm{SetCat}\left(1_{𝑜}\right)$$
2		df-ot	$$⊢⟨\varnothing ,\varnothing ,1_{𝑜}⟩=⟨⟨\varnothing ,\varnothing ⟩,1_{𝑜}⟩$$
3	2	sneqi	$$⊢\left\{⟨\varnothing ,\varnothing ,1_{𝑜}⟩\right\}=\left\{⟨⟨\varnothing ,\varnothing ⟩,1_{𝑜}⟩\right\}$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
6		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
7	6	fveq2i	$$⊢\mathrm{SetCat}\left(1_{𝑜}\right)=\mathrm{SetCat}\left(\left\{\varnothing \right\}\right)$$
8	1 7	eqtri	$$⊢\underset{\dot{}}{1}=\mathrm{SetCat}\left(\left\{\varnothing \right\}\right)$$
9		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
10	9	a1i	$$⊢\top \to \left\{\varnothing \right\}\in \mathrm{V}$$
11		eqid	$$⊢\mathrm{Hom}\left(\underset{\dot{}}{1}\right)=\mathrm{Hom}\left(\underset{\dot{}}{1}\right)$$
12	8 10 11	setchomfval	$$⊢\top \to \mathrm{Hom}\left(\underset{\dot{}}{1}\right)=\left(x\in \left\{\varnothing \right\},y\in \left\{\varnothing \right\}⟼y^x\right)$$
13	12	mptru	$$⊢\mathrm{Hom}\left(\underset{\dot{}}{1}\right)=\left(x\in \left\{\varnothing \right\},y\in \left\{\varnothing \right\}⟼y^x\right)$$
14		oveq2	$$⊢x=\varnothing \to y^x=y^{\varnothing }$$
15		oveq1	$$⊢y=\varnothing \to y^{\varnothing }={\varnothing }^{\varnothing }$$
16		0map0sn0	$$⊢{\varnothing }^{\varnothing }=\left\{\varnothing \right\}$$
17	16 6	eqtr4i	$$⊢{\varnothing }^{\varnothing }=1_{𝑜}$$
18	15 17	eqtrdi	$$⊢y=\varnothing \to y^{\varnothing }=1_{𝑜}$$
19	13 14 18	mposn	$$⊢\left(\varnothing \in \mathrm{V}\wedge \varnothing \in \mathrm{V}\wedge 1_{𝑜}\in \mathrm{V}\right)\to \mathrm{Hom}\left(\underset{\dot{}}{1}\right)=\left\{⟨⟨\varnothing ,\varnothing ⟩,1_{𝑜}⟩\right\}$$
20	4 4 5 19	mp3an	$$⊢\mathrm{Hom}\left(\underset{\dot{}}{1}\right)=\left\{⟨⟨\varnothing ,\varnothing ⟩,1_{𝑜}⟩\right\}$$
21	3 20	eqtr4i	$$⊢\left\{⟨\varnothing ,\varnothing ,1_{𝑜}⟩\right\}=\mathrm{Hom}\left(\underset{\dot{}}{1}\right)$$