Theorem catcofval

Description: Composition 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\}$$
	catcofval.x	$$⊢\underset{\dot{}}{·}\in \mathrm{V}$$
Assertion	catcofval	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\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		catcofval.x	$$⊢\underset{\dot{}}{·}\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		ccoid	$$⊢\mathrm{comp}=\mathrm{Slot}\mathrm{comp}\left(\mathrm{ndx}\right)$$
6		snsstp3	$$⊢\left\{⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\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{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}\subseteq C$$
8	4 5 7	strfv	$$⊢\underset{\dot{}}{·}\in \mathrm{V}\to \underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
9	2 8	ax-mp	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$