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	|- (/) e. _V
5		1oex	|- 1o e. _V
6		df1o2	|- 1o = { (/) }
7	6	fveq2i	|- ( SetCat ` 1o ) = ( SetCat ` { (/) } )
8	1 7	eqtri	|- .1. = ( SetCat ` { (/) } )
9		p0ex	|- { (/) } e. _V
10	9	a1i	|- ( T. -> { (/) } e. _V )
11		eqid	|- ( Hom ` .1. ) = ( Hom ` .1. )
12	8 10 11	setchomfval	|- ( T. -> ( Hom ` .1. ) = ( x e. { (/) } , y e. { (/) } |-> ( y ^m x ) ) )
13	12	mptru	|- ( Hom ` .1. ) = ( x e. { (/) } , y e. { (/) } |-> ( y ^m x ) )
14		oveq2	|- ( x = (/) -> ( y ^m x ) = ( y ^m (/) ) )
15		oveq1	|- ( y = (/) -> ( y ^m (/) ) = ( (/) ^m (/) ) )
16		0map0sn0	|- ( (/) ^m (/) ) = { (/) }
17	16 6	eqtr4i	|- ( (/) ^m (/) ) = 1o
18	15 17	eqtrdi	|- ( y = (/) -> ( y ^m (/) ) = 1o )
19	13 14 18	mposn	|- ( ( (/) e. _V /\ (/) e. _V /\ 1o e. _V ) -> ( Hom ` .1. ) = { <. <. (/) , (/) >. , 1o >. } )
20	4 4 5 19	mp3an	|- ( Hom ` .1. ) = { <. <. (/) , (/) >. , 1o >. }
21	3 20	eqtr4i	|- { <. (/) , (/) , 1o >. } = ( Hom ` .1. )