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)

	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		df-ot	$$⊢⟨M,M,{\mathrm{Base}}_M⟩=⟨⟨M,M⟩,{\mathrm{Base}}_M⟩$$
20	19	sneqi	$$⊢\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}=\left\{⟨⟨M,M⟩,{\mathrm{Base}}_M⟩\right\}$$
21	20	oveqi	$$⊢M\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}M=M\left\{⟨⟨M,M⟩,{\mathrm{Base}}_M⟩\right\}M$$
22		df-ov	$$⊢M\left\{⟨⟨M,M⟩,{\mathrm{Base}}_M⟩\right\}M=\left\{⟨⟨M,M⟩,{\mathrm{Base}}_M⟩\right\}\left(⟨M,M⟩\right)$$
23		opex	$$⊢⟨M,M⟩\in \mathrm{V}$$
24		fvex	$$⊢{\mathrm{Base}}_M\in \mathrm{V}$$
25	23 24	fvsn	$$⊢\left\{⟨⟨M,M⟩,{\mathrm{Base}}_M⟩\right\}\left(⟨M,M⟩\right)={\mathrm{Base}}_M$$
26	21 22 25	3eqtri	$$⊢M\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}M={\mathrm{Base}}_M$$
27	18 26	eqtrdi	$$⊢\phi \to XHY={\mathrm{Base}}_M$$