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