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	⊢ 𝐵 = ( Base ‘ 𝑀 )
	isnmnd.o	⊢ ⚬ = ( +g ‘ 𝑀 )
Assertion	isnmnd	⊢ ( ∀ 𝑧 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ( 𝑧 ⚬ 𝑥 ) ≠ 𝑥 → 𝑀 ∉ Mnd )

Proof

Step	Hyp	Ref	Expression
1		isnmnd.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		isnmnd.o	⊢ ⚬ = ( +g ‘ 𝑀 )
3		neneq	⊢ ( ( 𝑧 ⚬ 𝑥 ) ≠ 𝑥 → ¬ ( 𝑧 ⚬ 𝑥 ) = 𝑥 )
4	3	intnanrd	⊢ ( ( 𝑧 ⚬ 𝑥 ) ≠ 𝑥 → ¬ ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) )
5	4	reximi	⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑧 ⚬ 𝑥 ) ≠ 𝑥 → ∃ 𝑥 ∈ 𝐵 ¬ ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) )
6	5	ralimi	⊢ ( ∀ 𝑧 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ( 𝑧 ⚬ 𝑥 ) ≠ 𝑥 → ∀ 𝑧 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ¬ ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) )
7		rexnal	⊢ ( ∃ 𝑥 ∈ 𝐵 ¬ ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝐵 ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) )
8	7	ralbii	⊢ ( ∀ 𝑧 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ¬ ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐵 ¬ ∀ 𝑥 ∈ 𝐵 ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) )
9		ralnex	⊢ ( ∀ 𝑧 ∈ 𝐵 ¬ ∀ 𝑥 ∈ 𝐵 ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) ↔ ¬ ∃ 𝑧 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) )
10	8 9	bitri	⊢ ( ∀ 𝑧 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ¬ ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) ↔ ¬ ∃ 𝑧 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) )
11	6 10	sylib	⊢ ( ∀ 𝑧 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ( 𝑧 ⚬ 𝑥 ) ≠ 𝑥 → ¬ ∃ 𝑧 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) )
12	11	intnand	⊢ ( ∀ 𝑧 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ( 𝑧 ⚬ 𝑥 ) ≠ 𝑥 → ¬ ( 𝑀 ∈ Smgrp ∧ ∃ 𝑧 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) ) )
13	1 2	ismnddef	⊢ ( 𝑀 ∈ Mnd ↔ ( 𝑀 ∈ Smgrp ∧ ∃ 𝑧 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑧 ⚬ 𝑥 ) = 𝑥 ∧ ( 𝑥 ⚬ 𝑧 ) = 𝑥 ) ) )
14	12 13	sylnibr	⊢ ( ∀ 𝑧 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ( 𝑧 ⚬ 𝑥 ) ≠ 𝑥 → ¬ 𝑀 ∈ Mnd )
15		df-nel	⊢ ( 𝑀 ∉ Mnd ↔ ¬ 𝑀 ∈ Mnd )
16	14 15	sylibr	⊢ ( ∀ 𝑧 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ( 𝑧 ⚬ 𝑥 ) ≠ 𝑥 → 𝑀 ∉ Mnd )