Theorem mndideu

Description: The two-sided identity element of a monoid is unique. Lemma 2.2.1(a) of Herstein p. 55. (Contributed by Mario Carneiro, 8-Dec-2014)

	Ref	Expression
Hypotheses	mndcl.b	|- B = ( Base ` G )
	mndcl.p	|- .+ = ( +g ` G )
Assertion	mndideu	|- ( G e. Mnd -> E! u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) )

Proof

Step	Hyp	Ref	Expression
1		mndcl.b	|- B = ( Base ` G )
2		mndcl.p	|- .+ = ( +g ` G )
3	1 2	mndid	|- ( G e. Mnd -> E. u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) )
4		mgmidmo	|- E* u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x )
5		reu5	|- ( E! u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) <-> ( E. u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) /\ E* u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) ) )
6	3 4 5	sylanblrc	|- ( G e. Mnd -> E! u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) )