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

Metamath Proof Explorer

Theorem mndtcbasval

Description: The base set 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 )
mndtcbas.b 
|- ( ph -> B = ( Base ` C ) )
Assertion mndtcbasval 
|- ( ph -> B = { M } )

Proof

Step Hyp Ref Expression
1 mndtcbas.c 
 |-  ( ph -> C = ( MndToCat ` M ) )
2 mndtcbas.m 
 |-  ( ph -> M e. Mnd )
3 mndtcbas.b 
 |-  ( ph -> B = ( Base ` C ) )
4 1 2 mndtcval 
 |-  ( ph -> C = { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } )
5 4 fveq2d 
 |-  ( ph -> ( Base ` C ) = ( Base ` { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } ) )
6 snex 
 |-  { M } e. _V
7 catstr 
 |-  { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } Struct <. 1 , ; 1 5 >.
8 baseid 
 |-  Base = Slot ( Base ` ndx )
9 snsstp1 
 |-  { <. ( Base ` ndx ) , { M } >. } C_ { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. }
10 7 8 9 strfv 
 |-  ( { M } e. _V -> { M } = ( Base ` { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } ) )
11 6 10 mp1i 
 |-  ( ph -> { M } = ( Base ` { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } ) )
12 5 3 11 3eqtr4d 
 |-  ( ph -> B = { M } )