Metamath Proof Explorer

Theorem estrcval

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

Ref Expression
Hypotheses estrcval.c 
|- C = ( ExtStrCat ` U )
estrcval.u 
|- ( ph -> U e. V )
estrcval.h 
|- ( ph -> H = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
estrcval.o 
|- ( 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 ) ) ) )
Assertion estrcval 
|- ( ph -> C = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )

Proof

Step Hyp Ref Expression
1 estrcval.c 
 |-  C = ( ExtStrCat ` U )
2 estrcval.u 
 |-  ( ph -> U e. V )
3 estrcval.h 
 |-  ( ph -> H = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
4 estrcval.o 
 |-  ( 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 ) ) ) )
5 df-estrc 
 |-  ExtStrCat = ( u e. _V |-> { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. , <. ( 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 ) ) ) >. } )
6 simpr 
 |-  ( ( ph /\ u = U ) -> u = U )
7 6 opeq2d 
 |-  ( ( ph /\ u = U ) -> <. ( Base ` ndx ) , u >. = <. ( Base ` ndx ) , U >. )
8 eqidd 
 |-  ( ( ph /\ u = U ) -> ( ( Base ` y ) ^m ( Base ` x ) ) = ( ( Base ` y ) ^m ( Base ` x ) ) )
9 6 6 8 mpoeq123dv 
 |-  ( ( ph /\ u = U ) -> ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
10 3 adantr 
 |-  ( ( ph /\ u = U ) -> H = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
11 9 10 eqtr4d 
 |-  ( ( ph /\ u = U ) -> ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) = H )
12 11 opeq2d 
 |-  ( ( ph /\ u = U ) -> <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. = <. ( Hom ` ndx ) , H >. )
13 6 sqxpeqd 
 |-  ( ( ph /\ u = U ) -> ( u X. u ) = ( U X. U ) )
14 eqidd 
 |-  ( ( ph /\ u = U ) -> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) = ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) )
15 13 6 14 mpoeq123dv 
 |-  ( ( ph /\ u = U ) -> ( 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 ) ) ) )
16 4 adantr 
 |-  ( ( ph /\ u = U ) -> .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 ) ) ) )
17 15 16 eqtr4d 
 |-  ( ( ph /\ u = U ) -> ( 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 ) ) ) = .x. )
18 17 opeq2d 
 |-  ( ( ph /\ u = U ) -> <. ( 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 ) ) ) >. = <. ( comp ` ndx ) , .x. >. )
19 7 12 18 tpeq123d 
 |-  ( ( ph /\ u = U ) -> { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. , <. ( 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 ) ) ) >. } = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
20 2 elexd 
 |-  ( ph -> U e. _V )
21 tpex 
 |-  { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V
22 21 a1i 
 |-  ( ph -> { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V )
23 5 19 20 22 fvmptd2 
 |-  ( ph -> ( ExtStrCat ` U ) = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
24 1 23 syl5eq 
 |-  ( ph -> C = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )