setc1ohomfval

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

		Ref	Expression
	Hypothesis	funcsetc1o.1	$⊢ \underset{˙}{1} = SetCat (1_{𝑜})$
	Assertion	setc1ohomfval	$⊢ \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} = Hom (\underset{˙}{1})$

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

Metamath Proof Explorer