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

Metamath Proof Explorer

Theorem catcofval

Description: Composition 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. >. }
catcofval.x 
|- .x. e. _V
Assertion catcofval 
|- .x. = ( comp ` C )

Proof

Step Hyp Ref Expression
1 catbas.c 
 |-  C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. }
2 catcofval.x 
 |-  .x. 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 ccoid 
 |-  comp = Slot ( comp ` ndx )
6 snsstp3 
 |-  { <. ( comp ` ndx ) , .x. >. } C_ { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. }
7 6 1 sseqtrri 
 |-  { <. ( comp ` ndx ) , .x. >. } C_ C
8 4 5 7 strfv 
 |-  ( .x. e. _V -> .x. = ( comp ` C ) )
9 2 8 ax-mp 
 |-  .x. = ( comp ` C )