Metamath Proof Explorer

Theorem mndtcval

Description: Value of the category built from a monoid. (Contributed by Zhi Wang, 22-Sep-2024) (New usage is discouraged.)

Ref Expression
Hypotheses mndtcbas.c 
|- ( ph -> C = ( MndToCat ` M ) )
mndtcbas.m 
|- ( ph -> M e. Mnd )
Assertion mndtcval 
|- ( ph -> C = { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } )

Proof

Step Hyp Ref Expression
1 mndtcbas.c 
 |-  ( ph -> C = ( MndToCat ` M ) )
2 mndtcbas.m 
 |-  ( ph -> M e. Mnd )
3 sneq 
 |-  ( m = M -> { m } = { M } )
4 3 opeq2d 
 |-  ( m = M -> <. ( Base ` ndx ) , { m } >. = <. ( Base ` ndx ) , { M } >. )
5 id 
 |-  ( m = M -> m = M )
6 fveq2 
 |-  ( m = M -> ( Base ` m ) = ( Base ` M ) )
7 5 5 6 oteq123d 
 |-  ( m = M -> <. m , m , ( Base ` m ) >. = <. M , M , ( Base ` M ) >. )
8 7 sneqd 
 |-  ( m = M -> { <. m , m , ( Base ` m ) >. } = { <. M , M , ( Base ` M ) >. } )
9 8 opeq2d 
 |-  ( m = M -> <. ( Hom ` ndx ) , { <. m , m , ( Base ` m ) >. } >. = <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. )
10 5 5 5 oteq123d 
 |-  ( m = M -> <. m , m , m >. = <. M , M , M >. )
11 fveq2 
 |-  ( m = M -> ( +g ` m ) = ( +g ` M ) )
12 10 11 opeq12d 
 |-  ( m = M -> <. <. m , m , m >. , ( +g ` m ) >. = <. <. M , M , M >. , ( +g ` M ) >. )
13 12 sneqd 
 |-  ( m = M -> { <. <. m , m , m >. , ( +g ` m ) >. } = { <. <. M , M , M >. , ( +g ` M ) >. } )
14 13 opeq2d 
 |-  ( m = M -> <. ( comp ` ndx ) , { <. <. m , m , m >. , ( +g ` m ) >. } >. = <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. )
15 4 9 14 tpeq123d 
 |-  ( m = M -> { <. ( Base ` ndx ) , { m } >. , <. ( Hom ` ndx ) , { <. m , m , ( Base ` m ) >. } >. , <. ( comp ` ndx ) , { <. <. m , m , m >. , ( +g ` m ) >. } >. } = { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } )
16 df-mndtc 
 |-  MndToCat = ( m e. Mnd |-> { <. ( Base ` ndx ) , { m } >. , <. ( Hom ` ndx ) , { <. m , m , ( Base ` m ) >. } >. , <. ( comp ` ndx ) , { <. <. m , m , m >. , ( +g ` m ) >. } >. } )
17 tpex 
 |-  { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } e. _V
18 15 16 17 fvmpt 
 |-  ( M e. Mnd -> ( MndToCat ` M ) = { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } )
19 2 18 syl 
 |-  ( ph -> ( MndToCat ` M ) = { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } )
20 1 19 eqtrd 
 |-  ( ph -> C = { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } )