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	|- ( ph -> C = ( MndToCat ` M ) )
	mndtcbas.m	|- ( ph -> M e. Mnd )
	mndtcbas.b	|- ( ph -> B = ( Base ` C ) )
	mndtchom.x	|- ( ph -> X e. B )
	mndtchom.y	|- ( ph -> Y e. B )
Assertion	mndtcbas2	|- ( ph -> X = Y )

Proof

Step	Hyp	Ref	Expression
1		mndtcbas.c	|- ( ph -> C = ( MndToCat ` M ) )
2		mndtcbas.m	|- ( ph -> M e. Mnd )
3		mndtcbas.b	|- ( ph -> B = ( Base ` C ) )
4		mndtchom.x	|- ( ph -> X e. B )
5		mndtchom.y	|- ( ph -> Y e. B )
6	1 2 3	mndtcbas	|- ( ph -> E! x x e. B )
7		eumo	|- ( E! x x e. B -> E* x x e. B )
8		moel	|- ( E* x x e. B <-> A. x e. B A. y e. B x = y )
9	8	biimpi	|- ( E* x x e. B -> A. x e. B A. y e. B x = y )
10	6 7 9	3syl	|- ( ph -> A. x e. B A. y e. B x = y )
11		eqeq12	|- ( ( x = X /\ y = Y ) -> ( x = y <-> X = Y ) )
12	11	rspc2gv	|- ( ( X e. B /\ Y e. B ) -> ( A. x e. B A. y e. B x = y -> X = Y ) )
13	4 5 12	syl2anc	|- ( ph -> ( A. x e. B A. y e. B x = y -> X = Y ) )
14	10 13	mpd	|- ( ph -> X = Y )