This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 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 = 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 ∉ Mnd ↔ ¬ M ∈ 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 |-