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	mndtcbaseu.c	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
	mndtcbaseu.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
	mndtcbaseu.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
	mndtchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	mndtchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	mndtchom.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
Assertion	mndtchom	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( Base ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		mndtcbaseu.c	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
2		mndtcbaseu.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3		mndtcbaseu.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
4		mndtchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		mndtchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		mndtchom.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
7	1 2	mndtcval	⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , { 𝑀 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } ⟩ } )
8		catstr	⊢ { ⟨ ( Base ‘ ndx ) , { 𝑀 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } ⟩ } Struct ⟨ 1 , ; 1 5 ⟩
9		homid	⊢ Hom = Slot ( Hom ‘ ndx )
10		snsstp2	⊢ { ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , { 𝑀 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +_g ‘ 𝑀 ) ⟩ } ⟩ }
11		snex	⊢ { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ∈ V
12	11	a1i	⊢ ( 𝜑 → { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ∈ V )
13		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
14	7 8 9 10 12 13	strfv3	⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } )
15	6 14	eqtrd	⊢ ( 𝜑 → 𝐻 = { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } )
16	1 2 3 4	mndtcob	⊢ ( 𝜑 → 𝑋 = 𝑀 )
17	1 2 3 5	mndtcob	⊢ ( 𝜑 → 𝑌 = 𝑀 )
18	15 16 17	oveq123d	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑀 { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } 𝑀 ) )
19		fvex	⊢ ( Base ‘ 𝑀 ) ∈ V
20	19	ovsn2	⊢ ( 𝑀 { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } 𝑀 ) = ( Base ‘ 𝑀 )
21	18 20	eqtrdi	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( Base ‘ 𝑀 ) )

Metamath Proof Explorer

Theorem mndtchom

Proof