Theorem catbas

Description: The base 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\}$$
	catbas.b	$$⊢B\in \mathrm{V}$$
Assertion	catbas	$$⊢B={\mathrm{Base}}_C$$

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		catbas.b	$$⊢B\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		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
6		snsstp1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\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{Base}}_{\mathrm{ndx}},B⟩\right\}\subseteq C$$
8	4 5 7	strfv	$$⊢B\in \mathrm{V}\to B={\mathrm{Base}}_C$$
9	2 8	ax-mp	$$⊢B={\mathrm{Base}}_C$$