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	$$⊢\phi \to C=\mathrm{MndToCat}\left(M\right)$$
	mndtcbas.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
	mndtcbas.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
	mndtchom.x	$$⊢\phi \to X\in B$$
	mndtchom.y	$$⊢\phi \to Y\in B$$
	mndtchom.h	$$⊢\phi \to H=\mathrm{Hom}\left(C\right)$$
Assertion	mndtchom	$$⊢\phi \to XHY={\mathrm{Base}}_M$$

Proof

Step	Hyp	Ref	Expression
1		mndtcbas.c	$$⊢\phi \to C=\mathrm{MndToCat}\left(M\right)$$
2		mndtcbas.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
3		mndtcbas.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
4		mndtchom.x	$$⊢\phi \to X\in B$$
5		mndtchom.y	$$⊢\phi \to Y\in B$$
6		mndtchom.h	$$⊢\phi \to H=\mathrm{Hom}\left(C\right)$$
7	1 2	mndtcval	$$⊢\phi \to C=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{M\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}⟩\right\}$$
8		catstr	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{M\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}⟩\right\}\mathrm{Struct}⟨1,15⟩$$
9		homid	$$⊢\mathrm{Hom}=\mathrm{Slot}\mathrm{Hom}\left(\mathrm{ndx}\right)$$
10		snsstp2	$$⊢\left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{M\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}⟩\right\}$$
11		snex	$$⊢\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}\in \mathrm{V}$$
12	11	a1i	$$⊢\phi \to \left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}\in \mathrm{V}$$
13		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
14	7 8 9 10 12 13	strfv3	$$⊢\phi \to \mathrm{Hom}\left(C\right)=\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}$$
15	6 14	eqtrd	$$⊢\phi \to H=\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}$$
16	1 2 3 4	mndtcob	$$⊢\phi \to X=M$$
17	1 2 3 5	mndtcob	$$⊢\phi \to Y=M$$
18	15 16 17	oveq123d	$$⊢\phi \to XHY=M\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}M$$
19		fvex	$$⊢{\mathrm{Base}}_M\in \mathrm{V}$$
20	19	ovsn2	$$⊢M\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}M={\mathrm{Base}}_M$$
21	18 20	eqtrdi	$$⊢\phi \to XHY={\mathrm{Base}}_M$$