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

Proof

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

Metamath Proof Explorer

Theorem mndtchom

Proof