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	⊢ 𝐵 = ( Base ‘ 𝑀 )
	mgmcl.o	⊢ ⚬ = ( +g ‘ 𝑀 )
Assertion	isnmgm	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 ⚬ 𝑌 ) ∉ 𝐵 ) → 𝑀 ∉ Mgm )

Proof

Step	Hyp	Ref	Expression
1		mgmcl.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		mgmcl.o	⊢ ⚬ = ( +g ‘ 𝑀 )
3	1 2	mgmcl	⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝐵 )
4	3	3expib	⊢ ( 𝑀 ∈ Mgm → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝐵 ) )
5	4	com12	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 ∈ Mgm → ( 𝑋 ⚬ 𝑌 ) ∈ 𝐵 ) )
6	5	nelcon3d	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ⚬ 𝑌 ) ∉ 𝐵 → 𝑀 ∉ Mgm ) )
7	6	3impia	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 ⚬ 𝑌 ) ∉ 𝐵 ) → 𝑀 ∉ Mgm )