catbas

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

	Ref	Expression
Hypotheses	catbas.c	$⊢ C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
	catbas.b	$⊢ B \in V$
Assertion	catbas	$⊢ B = {Base}_{C}$

Step	Hyp	Ref	Expression
1		catbas.c	$⊢ C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
2		catbas.b	$⊢ B \in V$
3		catstr	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} Struct ⟨1, 15⟩$
4	1 3	eqbrtri	$⊢ C Struct ⟨1, 15⟩$
5		baseid	$⊢ Base = Slot {Base}_{ndx}$
6		snsstp1	$⊢ \{⟨{Base}_{ndx}, B⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
7	6 1	sseqtrri	$⊢ \{⟨{Base}_{ndx}, B⟩\} \subseteq C$
8	4 5 7	strfv	$⊢ B \in V \to B = {Base}_{C}$
9	2 8	ax-mp	$⊢ B = {Base}_{C}$

Metamath Proof Explorer