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 } )