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={\mathrm{Base}}_M$$
	isnmnd.o	No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion	isnmnd	Could not format assertion : No typesetting found for |- ( A. z e. B E. x e. B ( z .o. x ) =/= x -> M e/ Mnd ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		isnmnd.b	$$⊢B={\mathrm{Base}}_M$$
2		isnmnd.o	Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |-
3		neneq	Could not format ( ( z .o. x ) =/= x -> -. ( z .o. x ) = x ) : No typesetting found for |- ( ( z .o. x ) =/= x -> -. ( z .o. x ) = x ) with typecode |-
4	3	intnanrd	Could not format ( ( z .o. x ) =/= x -> -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) ) : No typesetting found for |- ( ( z .o. x ) =/= x -> -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) ) with typecode |-
5	4	reximi	Could not format ( E. x e. B ( z .o. x ) =/= x -> E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) ) : No typesetting found for |- ( E. x e. B ( z .o. x ) =/= x -> E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) ) with typecode |-
6	5	ralimi	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
7		rexnal	Could not format ( E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) <-> -. A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) ) : No typesetting found for |- ( E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) <-> -. A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) ) with typecode |-
8	7	ralbii	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
9		ralnex	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
10	8 9	bitri	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
11	6 10	sylib	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
12	11	intnand	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
13	1 2	ismnddef	Could not format ( M e. Mnd <-> ( M e. Smgrp /\ E. z e. B A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) ) ) : No typesetting found for |- ( M e. Mnd <-> ( M e. Smgrp /\ E. z e. B A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) ) ) with typecode |-
14	12 13	sylnibr	Could not format ( A. z e. B E. x e. B ( z .o. x ) =/= x -> -. M e. Mnd ) : No typesetting found for |- ( A. z e. B E. x e. B ( z .o. x ) =/= x -> -. M e. Mnd ) with typecode |-
15		df-nel	$$⊢M\notin \mathrm{Mnd}\leftrightarrow \neg M\in \mathrm{Mnd}$$
16	14 15	sylibr	Could not format ( A. z e. B E. x e. B ( z .o. x ) =/= x -> M e/ Mnd ) : No typesetting found for |- ( A. z e. B E. x e. B ( z .o. x ) =/= x -> M e/ Mnd ) with typecode |-