Metamath Proof Explorer

Theorem sgrpnmndex

Description: There is a semigroup which is not a monoid. (Contributed by AV, 29-Jan-2020)

Ref Expression
Assertion sgrpnmndex ∃ 𝑚 ∈ Smgrp 𝑚 ∉ Mnd

Proof

Step Hyp Ref Expression
1 prhash2ex ⊢ ( ♯ ‘ { 0 , 1 } ) = 2
2 eqid ⊢ { 0 , 1 } = { 0 , 1 }
3 prex ⊢ { 0 , 1 } ∈ V
4 eqeq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 = 0 ↔ 𝑢 = 0 ) )
5 4 ifbid ⊢ ( 𝑥 = 𝑢 → if ( 𝑥 = 0 , 0 , 1 ) = if ( 𝑢 = 0 , 0 , 1 ) )
6 eqidd ⊢ ( 𝑦 = 𝑣 → if ( 𝑢 = 0 , 0 , 1 ) = if ( 𝑢 = 0 , 0 , 1 ) )
7 5 6 cbvmpov ⊢ ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) = ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) )
8 7 opeq2i ⊢ ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ = ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) ⟩
9 8 preq2i ⊢ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) ⟩ }
10 9 grpbase ⊢ ( { 0 , 1 } ∈ V → { 0 , 1 } = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ } ) )
11 3 10 ax-mp ⊢ { 0 , 1 } = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ } )
12 11 eqcomi ⊢ ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ } ) = { 0 , 1 }
13 3 3 mpoex ⊢ ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) ∈ V
14 9 grpplusg ⊢ ( ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) ∈ V → ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ } ) )
15 13 14 ax-mp ⊢ ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ } )
16 15 eqcomi ⊢ ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ } ) = ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( 𝑢 = 0 , 0 , 1 ) )
17 2 12 16 sgrp2nmndlem4 ⊢ ( ( ♯ ‘ { 0 , 1 } ) = 2 → { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ } ∈ Smgrp )
18 neleq1 ⊢ ( 𝑚 = { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ } → ( 𝑚 ∉ Mnd ↔ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ } ∉ Mnd ) )
19 18 adantl ⊢ ( ( ( ♯ ‘ { 0 , 1 } ) = 2 ∧ 𝑚 = { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ } ) → ( 𝑚 ∉ Mnd ↔ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ } ∉ Mnd ) )
20 2 12 16 sgrp2nmndlem5 ⊢ ( ( ♯ ‘ { 0 , 1 } ) = 2 → { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( 𝑥 = 0 , 0 , 1 ) ) ⟩ } ∉ Mnd )
21 17 19 20 rspcedvd ⊢ ( ( ♯ ‘ { 0 , 1 } ) = 2 → ∃ 𝑚 ∈ Smgrp 𝑚 ∉ Mnd )
22 1 21 ax-mp ⊢ ∃ 𝑚 ∈ Smgrp 𝑚 ∉ Mnd