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

Metamath Proof Explorer

Theorem cathomfval

Description: The hom-sets 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. >. }
cathomfval.h 
|- H e. _V
Assertion cathomfval 
|- H = ( Hom ` C )

Proof

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