Metamath Proof Explorer

Theorem mgmnsgrpex

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

Ref Expression
Assertion mgmnsgrpex ∃ 𝑚 ∈ Mgm 𝑚 ∉ Smgrp

Proof

Step Hyp Ref Expression
1 prhash2ex ⊢ ( ♯ ‘ { 0 , 1 } ) = 2
2 c0ex ⊢ 0 ∈ V
3 1ex ⊢ 1 ∈ V
4 2 3 pm3.2i ⊢ ( 0 ∈ V ∧ 1 ∈ V )
5 eqid ⊢ { 0 , 1 } = { 0 , 1 }
6 prex ⊢ { 0 , 1 } ∈ V
7 eqeq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 = 0 ↔ 𝑢 = 0 ) )
8 7 anbi1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) ↔ ( 𝑢 = 0 ∧ 𝑦 = 0 ) ) )
9 8 ifbid ⊢ ( 𝑥 = 𝑢 → if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) = if ( ( 𝑢 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) )
10 eqeq1 ⊢ ( 𝑦 = 𝑣 → ( 𝑦 = 0 ↔ 𝑣 = 0 ) )
11 10 anbi2d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑢 = 0 ∧ 𝑦 = 0 ) ↔ ( 𝑢 = 0 ∧ 𝑣 = 0 ) ) )
12 11 ifbid ⊢ ( 𝑦 = 𝑣 → if ( ( 𝑢 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) = if ( ( 𝑢 = 0 ∧ 𝑣 = 0 ) , 1 , 0 ) )
13 9 12 cbvmpov ⊢ ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) = ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( ( 𝑢 = 0 ∧ 𝑣 = 0 ) , 1 , 0 ) )
14 13 opeq2i ⊢ ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ = ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( ( 𝑢 = 0 ∧ 𝑣 = 0 ) , 1 , 0 ) ) ⟩
15 14 preq2i ⊢ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( ( 𝑢 = 0 ∧ 𝑣 = 0 ) , 1 , 0 ) ) ⟩ }
16 15 grpbase ⊢ ( { 0 , 1 } ∈ V → { 0 , 1 } = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } ) )
17 6 16 ax-mp ⊢ { 0 , 1 } = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } )
18 17 eqcomi ⊢ ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } ) = { 0 , 1 }
19 6 6 mpoex ⊢ ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( ( 𝑢 = 0 ∧ 𝑣 = 0 ) , 1 , 0 ) ) ∈ V
20 15 grpplusg ⊢ ( ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( ( 𝑢 = 0 ∧ 𝑣 = 0 ) , 1 , 0 ) ) ∈ V → ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( ( 𝑢 = 0 ∧ 𝑣 = 0 ) , 1 , 0 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } ) )
21 19 20 ax-mp ⊢ ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( ( 𝑢 = 0 ∧ 𝑣 = 0 ) , 1 , 0 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } )
22 21 eqcomi ⊢ ( +g ‘ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } ) = ( 𝑢 ∈ { 0 , 1 } , 𝑣 ∈ { 0 , 1 } ↦ if ( ( 𝑢 = 0 ∧ 𝑣 = 0 ) , 1 , 0 ) )
23 5 18 22 mgm2nsgrplem1 ⊢ ( ( 0 ∈ V ∧ 1 ∈ V ) → { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } ∈ Mgm )
24 4 23 mp1i ⊢ ( ( ♯ ‘ { 0 , 1 } ) = 2 → { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } ∈ Mgm )
25 neleq1 ⊢ ( 𝑚 = { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } → ( 𝑚 ∉ Smgrp ↔ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } ∉ Smgrp ) )
26 25 adantl ⊢ ( ( ( ♯ ‘ { 0 , 1 } ) = 2 ∧ 𝑚 = { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } ) → ( 𝑚 ∉ Smgrp ↔ { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } ∉ Smgrp ) )
27 5 18 22 mgm2nsgrplem4 ⊢ ( ( ♯ ‘ { 0 , 1 } ) = 2 → { ⟨ ( Base ‘ ndx ) , { 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ { 0 , 1 } , 𝑦 ∈ { 0 , 1 } ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 1 , 0 ) ) ⟩ } ∉ Smgrp )
28 24 26 27 rspcedvd ⊢ ( ( ♯ ‘ { 0 , 1 } ) = 2 → ∃ 𝑚 ∈ Mgm 𝑚 ∉ Smgrp )
29 1 28 ax-mp ⊢ ∃ 𝑚 ∈ Mgm 𝑚 ∉ Smgrp