Theorem setc1ohomfval

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

	Ref	Expression
Hypothesis	funcsetc1o.1	⊢ 1 = ( SetCat ‘ 1o )
Assertion	setc1ohomfval	⊢ { ⟨ ∅ , ∅ , 1o ⟩ } = ( Hom ‘ 1 )

Proof

Step	Hyp	Ref	Expression
1		funcsetc1o.1	⊢ 1 = ( SetCat ‘ 1o )
2		df-ot	⊢ ⟨ ∅ , ∅ , 1o ⟩ = ⟨ ⟨ ∅ , ∅ ⟩ , 1o ⟩
3	2	sneqi	⊢ { ⟨ ∅ , ∅ , 1o ⟩ } = { ⟨ ⟨ ∅ , ∅ ⟩ , 1o ⟩ }
4		0ex	⊢ ∅ ∈ V
5		1oex	⊢ 1o ∈ V
6		df1o2	⊢ 1o = { ∅ }
7	6	fveq2i	⊢ ( SetCat ‘ 1o ) = ( SetCat ‘ { ∅ } )
8	1 7	eqtri	⊢ 1 = ( SetCat ‘ { ∅ } )
9		p0ex	⊢ { ∅ } ∈ V
10	9	a1i	⊢ ( ⊤ → { ∅ } ∈ V )
11		eqid	⊢ ( Hom ‘ 1 ) = ( Hom ‘ 1 )
12	8 10 11	setchomfval	⊢ ( ⊤ → ( Hom ‘ 1 ) = ( 𝑥 ∈ { ∅ } , 𝑦 ∈ { ∅ } ↦ ( 𝑦 ↑m 𝑥 ) ) )
13	12	mptru	⊢ ( Hom ‘ 1 ) = ( 𝑥 ∈ { ∅ } , 𝑦 ∈ { ∅ } ↦ ( 𝑦 ↑m 𝑥 ) )
14		oveq2	⊢ ( 𝑥 = ∅ → ( 𝑦 ↑m 𝑥 ) = ( 𝑦 ↑m ∅ ) )
15		oveq1	⊢ ( 𝑦 = ∅ → ( 𝑦 ↑m ∅ ) = ( ∅ ↑m ∅ ) )
16		0map0sn0	⊢ ( ∅ ↑m ∅ ) = { ∅ }
17	16 6	eqtr4i	⊢ ( ∅ ↑m ∅ ) = 1o
18	15 17	eqtrdi	⊢ ( 𝑦 = ∅ → ( 𝑦 ↑m ∅ ) = 1o )
19	13 14 18	mposn	⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ∧ 1o ∈ V ) → ( Hom ‘ 1 ) = { ⟨ ⟨ ∅ , ∅ ⟩ , 1o ⟩ } )
20	4 4 5 19	mp3an	⊢ ( Hom ‘ 1 ) = { ⟨ ⟨ ∅ , ∅ ⟩ , 1o ⟩ }
21	3 20	eqtr4i	⊢ { ⟨ ∅ , ∅ , 1o ⟩ } = ( Hom ‘ 1 )