Theorem mndtcbas2

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

	Ref	Expression
Hypotheses	mndtcbas.c	No typesetting found for |- ( ph -> C = ( MndToCat ` M ) ) with typecode |-
	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$$
Assertion	mndtcbas2	$$⊢\phi \to X=Y$$

Proof

Step	Hyp	Ref	Expression
1		mndtcbas.c	Could not format ( ph -> C = ( MndToCat ` M ) ) : No typesetting found for |- ( ph -> C = ( MndToCat ` M ) ) with typecode |-
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	1 2 3	mndtcbas	$$⊢\phi \to \exists !xx\in B$$
7		eumo	$$⊢\exists !xx\in B\to {\exists }^{*}xx\in B$$
8		moel	$$⊢{\exists }^{*}xx\in B\leftrightarrow \forall x\in B\forall y\in Bx=y$$
9	8	biimpi	$$⊢{\exists }^{*}xx\in B\to \forall x\in B\forall y\in Bx=y$$
10	6 7 9	3syl	$$⊢\phi \to \forall x\in B\forall y\in Bx=y$$
11		eqeq12	$$⊢\left(x=X\wedge y=Y\right)\to \left(x=y\leftrightarrow X=Y\right)$$
12	11	rspc2gv	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall x\in B\forall y\in Bx=y\to X=Y\right)$$
13	4 5 12	syl2anc	$$⊢\phi \to \left(\forall x\in B\forall y\in Bx=y\to X=Y\right)$$
14	10 13	mpd	$$⊢\phi \to X=Y$$