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

Metamath Proof Explorer

Theorem isnmgm

Description: A condition for a structure not to be a magma. (Contributed by AV, 30-Jan-2020) (Proof shortened by NM, 5-Feb-2020)

Ref Expression
Hypotheses mgmcl.b ⊢ B = Base M
mgmcl.o No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion isnmgm Could not format assertion : No typesetting found for |- ( ( X e. B /\ Y e. B /\ ( X .o. Y ) e/ B ) -> M e/ Mgm ) with typecode |-

Proof

Step Hyp Ref Expression
1 mgmcl.b ⊢ B = Base M
2 mgmcl.o Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |-
3 1 2 mgmcl Could not format ( ( M e. Mgm /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B ) : No typesetting found for |- ( ( M e. Mgm /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B ) with typecode |-
4 3 3expib Could not format ( M e. Mgm -> ( ( X e. B /\ Y e. B ) -> ( X .o. Y ) e. B ) ) : No typesetting found for |- ( M e. Mgm -> ( ( X e. B /\ Y e. B ) -> ( X .o. Y ) e. B ) ) with typecode |-
5 4 com12 Could not format ( ( X e. B /\ Y e. B ) -> ( M e. Mgm -> ( X .o. Y ) e. B ) ) : No typesetting found for |- ( ( X e. B /\ Y e. B ) -> ( M e. Mgm -> ( X .o. Y ) e. B ) ) with typecode |-
6 5 nelcon3d Could not format ( ( X e. B /\ Y e. B ) -> ( ( X .o. Y ) e/ B -> M e/ Mgm ) ) : No typesetting found for |- ( ( X e. B /\ Y e. B ) -> ( ( X .o. Y ) e/ B -> M e/ Mgm ) ) with typecode |-
7 6 3impia Could not format ( ( X e. B /\ Y e. B /\ ( X .o. Y ) e/ B ) -> M e/ Mgm ) : No typesetting found for |- ( ( X e. B /\ Y e. B /\ ( X .o. Y ) e/ B ) -> M e/ Mgm ) with typecode |-