Theorem mndtchom

Description: The only hom-set of the category built from a monoid is the base set of the monoid. (Contributed by Zhi Wang, 22-Sep-2024) (Proof shortened by Zhi Wang, 22-Oct-2025)

	Ref	Expression
Hypotheses	mndtcbas.c	|- ( ph -> C = ( MndToCat ` M ) )
	mndtcbas.m	|- ( ph -> M e. Mnd )
	mndtcbas.b	|- ( ph -> B = ( Base ` C ) )
	mndtchom.x	|- ( ph -> X e. B )
	mndtchom.y	|- ( ph -> Y e. B )
	mndtchom.h	|- ( ph -> H = ( Hom ` C ) )
Assertion	mndtchom	|- ( ph -> ( X H Y ) = ( Base ` 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		mndtchom.x	|- ( ph -> X e. B )
5		mndtchom.y	|- ( ph -> Y e. B )
6		mndtchom.h	|- ( ph -> H = ( Hom ` C ) )
7	1 2	mndtcval	|- ( ph -> C = { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } )
8		catstr	|- { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } Struct <. 1 , ; 1 5 >.
9		homid	|- Hom = Slot ( Hom ` ndx )
10		snsstp2	|- { <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. } C_ { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. }
11		snex	|- { <. M , M , ( Base ` M ) >. } e. _V
12	11	a1i	|- ( ph -> { <. M , M , ( Base ` M ) >. } e. _V )
13		eqid	|- ( Hom ` C ) = ( Hom ` C )
14	7 8 9 10 12 13	strfv3	|- ( ph -> ( Hom ` C ) = { <. M , M , ( Base ` M ) >. } )
15	6 14	eqtrd	|- ( ph -> H = { <. M , M , ( Base ` M ) >. } )
16	1 2 3 4	mndtcob	|- ( ph -> X = M )
17	1 2 3 5	mndtcob	|- ( ph -> Y = M )
18	15 16 17	oveq123d	|- ( ph -> ( X H Y ) = ( M { <. M , M , ( Base ` M ) >. } M ) )
19		fvex	|- ( Base ` M ) e. _V
20	19	ovsn2	|- ( M { <. M , M , ( Base ` M ) >. } M ) = ( Base ` M )
21	18 20	eqtrdi	|- ( ph -> ( X H Y ) = ( Base ` M ) )