Theorem isnmnd

Description: A condition for a structure not to be a monoid: every element of the base set is not a left identity for at least one element of the base set. (Contributed by AV, 4-Feb-2020)

	Ref	Expression
Hypotheses	isnmnd.b	|- B = ( Base ` M )
	isnmnd.o	|- .o. = ( +g ` M )
Assertion	isnmnd	|- ( A. z e. B E. x e. B ( z .o. x ) =/= x -> M e/ Mnd )

Proof

Step	Hyp	Ref	Expression
1		isnmnd.b	|- B = ( Base ` M )
2		isnmnd.o	|- .o. = ( +g ` M )
3		neneq	|- ( ( z .o. x ) =/= x -> -. ( z .o. x ) = x )
4	3	intnanrd	|- ( ( z .o. x ) =/= x -> -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
5	4	reximi	|- ( E. x e. B ( z .o. x ) =/= x -> E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
6	5	ralimi	|- ( A. z e. B E. x e. B ( z .o. x ) =/= x -> A. z e. B E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
7		rexnal	|- ( E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) <-> -. A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
8	7	ralbii	|- ( A. z e. B E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) <-> A. z e. B -. A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
9		ralnex	|- ( A. z e. B -. A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) <-> -. E. z e. B A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
10	8 9	bitri	|- ( A. z e. B E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) <-> -. E. z e. B A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
11	6 10	sylib	|- ( A. z e. B E. x e. B ( z .o. x ) =/= x -> -. E. z e. B A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
12	11	intnand	|- ( A. z e. B E. x e. B ( z .o. x ) =/= x -> -. ( M e. Smgrp /\ E. z e. B A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) ) )
13	1 2	ismnddef	|- ( M e. Mnd <-> ( M e. Smgrp /\ E. z e. B A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) ) )
14	12 13	sylnibr	|- ( A. z e. B E. x e. B ( z .o. x ) =/= x -> -. M e. Mnd )
15		df-nel	|- ( M e/ Mnd <-> -. M e. Mnd )
16	14 15	sylibr	|- ( A. z e. B E. x e. B ( z .o. x ) =/= x -> M e/ Mnd )