Metamath Proof Explorer

Theorem estrccofval

Description: Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020)

Ref Expression
Hypotheses estrcbas.c 
|- C = ( ExtStrCat ` U )
estrcbas.u 
|- ( ph -> U e. V )
estrcco.o 
|- .x. = ( comp ` C )
Assertion estrccofval 
|- ( ph -> .x. = ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) )

Proof

Step Hyp Ref Expression
1 estrcbas.c 
 |-  C = ( ExtStrCat ` U )
2 estrcbas.u 
 |-  ( ph -> U e. V )
3 estrcco.o 
 |-  .x. = ( comp ` C )
4 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
5 1 2 4 estrchomfval 
 |-  ( ph -> ( Hom ` C ) = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
6 eqidd 
 |-  ( ph -> ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) = ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) )
7 1 2 5 6 estrcval 
 |-  ( ph -> C = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) >. } )
8 catstr 
 |-  { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) >. } Struct <. 1 , ; 1 5 >.
9 ccoid 
 |-  comp = Slot ( comp ` ndx )
10 snsstp3 
 |-  { <. ( comp ` ndx ) , ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) >. } C_ { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) >. }
11 2 2 xpexd 
 |-  ( ph -> ( U X. U ) e. _V )
12 mpoexga 
 |-  ( ( ( U X. U ) e. _V /\ U e. V ) -> ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) e. _V )
13 11 2 12 syl2anc 
 |-  ( ph -> ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) e. _V )
14 7 8 9 10 13 3 strfv3 
 |-  ( ph -> .x. = ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) )