Theorem cathomfval

Description: The hom-sets of the category structure. (Contributed by Zhi Wang, 5-Nov-2025)

	Ref	Expression
Hypotheses	catbas.c	$$⊢C=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}$$
	cathomfval.h	$$⊢H\in \mathrm{V}$$
Assertion	cathomfval	$$⊢H=\mathrm{Hom}\left(C\right)$$

Proof

Step	Hyp	Ref	Expression
1		catbas.c	$$⊢C=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}$$
2		cathomfval.h	$$⊢H\in \mathrm{V}$$
3		catstr	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}\mathrm{Struct}⟨1,15⟩$$
4	1 3	eqbrtri	$$⊢C\mathrm{Struct}⟨1,15⟩$$
5		homid	$$⊢\mathrm{Hom}=\mathrm{Slot}\mathrm{Hom}\left(\mathrm{ndx}\right)$$
6		snsstp2	$$⊢\left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}$$
7	6 1	sseqtrri	$$⊢\left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right\}\subseteq C$$
8	4 5 7	strfv	$$⊢H\in \mathrm{V}\to H=\mathrm{Hom}\left(C\right)$$
9	2 8	ax-mp	$$⊢H=\mathrm{Hom}\left(C\right)$$