This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ) , .x. >. }
catbas.b 
|- B e. _V
Assertion catbas 
|- B = ( Base ` C )

Proof

Step Hyp Ref Expression
1 catbas.c 
 |-  C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. }
2 catbas.b 
 |-  B e. _V
3 catstr 
 |-  { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } Struct <. 1 , ; 1 5 >.
4 1 3 eqbrtri 
 |-  C Struct <. 1 , ; 1 5 >.
5 baseid 
 |-  Base = Slot ( Base ` ndx )
6 snsstp1 
 |-  { <. ( Base ` ndx ) , B >. } C_ { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. }
7 6 1 sseqtrri 
 |-  { <. ( Base ` ndx ) , B >. } C_ C
8 4 5 7 strfv 
 |-  ( B e. _V -> B = ( Base ` C ) )
9 2 8 ax-mp 
 |-  B = ( Base ` C )