Theorem mndtcobeq

Description: Two objects in a category built from a monoid are identical. (Contributed by Zhi Wang, 24-Sep-2024)

	Ref	Expression
Hypotheses	mndtcbaseu.c	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
	mndtcbaseu.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
	mndtcbaseu.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
	mndtchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	mndtchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	mndtcobeq	⊢ ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		mndtcbaseu.c	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
2		mndtcbaseu.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3		mndtcbaseu.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
4		mndtchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		mndtchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6	1 2 3	mndtcbaseu	⊢ ( 𝜑 → ∃! 𝑥 𝑥 ∈ 𝐵 )
7		eumo	⊢ ( ∃! 𝑥 𝑥 ∈ 𝐵 → ∃* 𝑥 𝑥 ∈ 𝐵 )
8		moel	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 )
9	8	biimpi	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐵 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 )
10	6 7 9	3syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 )
11		eqeq12	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑥 = 𝑦 ↔ 𝑋 = 𝑌 ) )
12	11	rspc2gv	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 → 𝑋 = 𝑌 ) )
13	4 5 12	syl2anc	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 → 𝑋 = 𝑌 ) )
14	10 13	mpd	⊢ ( 𝜑 → 𝑋 = 𝑌 )