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	|- .o. = ( +g ` M )
Assertion	isnmgm	|- ( ( X e. B /\ Y e. B /\ ( X .o. Y ) e/ B ) -> M e/ Mgm )

Proof

Step	Hyp	Ref	Expression
1		mgmcl.b	|- B = ( Base ` M )
2		mgmcl.o	|- .o. = ( +g ` M )
3	1 2	mgmcl	|- ( ( M e. Mgm /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B )
4	3	3expib	|- ( M e. Mgm -> ( ( X e. B /\ Y e. B ) -> ( X .o. Y ) e. B ) )
5	4	com12	|- ( ( X e. B /\ Y e. B ) -> ( M e. Mgm -> ( X .o. Y ) e. B ) )
6	5	nelcon3d	|- ( ( X e. B /\ Y e. B ) -> ( ( X .o. Y ) e/ B -> M e/ Mgm ) )
7	6	3impia	|- ( ( X e. B /\ Y e. B /\ ( X .o. Y ) e/ B ) -> M e/ Mgm )