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 ⊢ 𝐵 = ( 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 )