Theorem mgmnsgrpex

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

	Ref	Expression
Assertion	mgmnsgrpex	Could not format assertion : No typesetting found for |- E. m e. Mgm m e/ Smgrp with typecode |-

Proof

Step	Hyp	Ref	Expression
1		prhash2ex	$$⊢\left|\left\{0,1\right\}\right|=2$$
2		c0ex	$$⊢0\in \mathrm{V}$$
3		1ex	$$⊢1\in \mathrm{V}$$
4	2 3	pm3.2i	$$⊢\left(0\in \mathrm{V}\wedge 1\in \mathrm{V}\right)$$
5		eqid	$$⊢\left\{0,1\right\}=\left\{0,1\right\}$$
6		prex	$$⊢\left\{0,1\right\}\in \mathrm{V}$$
7		eqeq1	$$⊢x=u\to \left(x=0\leftrightarrow u=0\right)$$
8	7	anbi1d	$$⊢x=u\to \left(\left(x=0\wedge y=0\right)\leftrightarrow \left(u=0\wedge y=0\right)\right)$$
9	8	ifbid	$$⊢x=u\to if\left(\left(x=0\wedge y=0\right),1,0\right)=if\left(\left(u=0\wedge y=0\right),1,0\right)$$
10		eqeq1	$$⊢y=v\to \left(y=0\leftrightarrow v=0\right)$$
11	10	anbi2d	$$⊢y=v\to \left(\left(u=0\wedge y=0\right)\leftrightarrow \left(u=0\wedge v=0\right)\right)$$
12	11	ifbid	$$⊢y=v\to if\left(\left(u=0\wedge y=0\right),1,0\right)=if\left(\left(u=0\wedge v=0\right),1,0\right)$$
13	9 12	cbvmpov	$$⊢\left(x\in \left\{0,1\right\},y\in \left\{0,1\right\}⟼if\left(\left(x=0\wedge y=0\right),1,0\right)\right)=\left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(\left(u=0\wedge v=0\right),1,0\right)\right)$$
14	13	opeq2i	$$⊢⟨{+}_{\mathrm{ndx}},\left(x\in \left\{0,1\right\},y\in \left\{0,1\right\}⟼if\left(\left(x=0\wedge y=0\right),1,0\right)\right)⟩=⟨{+}_{\mathrm{ndx}},\left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(\left(u=0\wedge v=0\right),1,0\right)\right)⟩$$
15	14	preq2i	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\left(x\in \left\{0,1\right\},y\in \left\{0,1\right\}⟼if\left(\left(x=0\wedge y=0\right),1,0\right)\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(\left(u=0\wedge v=0\right),1,0\right)\right)⟩\right\}$$
16	15	grpbase	$$⊢\left\{0,1\right\}\in \mathrm{V}\to \left\{0,1\right\}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\left(x\in \left\{0,1\right\},y\in \left\{0,1\right\}⟼if\left(\left(x=0\wedge y=0\right),1,0\right)\right)⟩\right\}}$$
17	6 16	ax-mp	$$⊢\left\{0,1\right\}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\left(x\in \left\{0,1\right\},y\in \left\{0,1\right\}⟼if\left(\left(x=0\wedge y=0\right),1,0\right)\right)⟩\right\}}$$
18	17	eqcomi	$$⊢{\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\left(x\in \left\{0,1\right\},y\in \left\{0,1\right\}⟼if\left(\left(x=0\wedge y=0\right),1,0\right)\right)⟩\right\}}=\left\{0,1\right\}$$
19	6 6	mpoex	$$⊢\left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(\left(u=0\wedge v=0\right),1,0\right)\right)\in \mathrm{V}$$
20	15	grpplusg	$$⊢\left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(\left(u=0\wedge v=0\right),1,0\right)\right)\in \mathrm{V}\to \left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(\left(u=0\wedge v=0\right),1,0\right)\right)={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\left(x\in \left\{0,1\right\},y\in \left\{0,1\right\}⟼if\left(\left(x=0\wedge y=0\right),1,0\right)\right)⟩\right\}}$$
21	19 20	ax-mp	$$⊢\left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(\left(u=0\wedge v=0\right),1,0\right)\right)={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\left(x\in \left\{0,1\right\},y\in \left\{0,1\right\}⟼if\left(\left(x=0\wedge y=0\right),1,0\right)\right)⟩\right\}}$$
22	21	eqcomi	$$⊢{+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\left(x\in \left\{0,1\right\},y\in \left\{0,1\right\}⟼if\left(\left(x=0\wedge y=0\right),1,0\right)\right)⟩\right\}}=\left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(\left(u=0\wedge v=0\right),1,0\right)\right)$$
23	5 18 22	mgm2nsgrplem1	$$⊢\left(0\in \mathrm{V}\wedge 1\in \mathrm{V}\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\left(x\in \left\{0,1\right\},y\in \left\{0,1\right\}⟼if\left(\left(x=0\wedge y=0\right),1,0\right)\right)⟩\right\}\in \mathrm{Mgm}$$
24	4 23	mp1i	$$⊢\left|\left\{0,1\right\}\right|=2\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\left(x\in \left\{0,1\right\},y\in \left\{0,1\right\}⟼if\left(\left(x=0\wedge y=0\right),1,0\right)\right)⟩\right\}\in \mathrm{Mgm}$$
25		neleq1	Could not format ( m = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } -> ( m e/ Smgrp <-> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } e/ Smgrp ) ) : No typesetting found for |- ( m = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } -> ( m e/ Smgrp <-> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } e/ Smgrp ) ) with typecode |-
26	25	adantl	Could not format ( ( ( # ` { 0 , 1 } ) = 2 /\ m = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } ) -> ( m e/ Smgrp <-> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } e/ Smgrp ) ) : No typesetting found for |- ( ( ( # ` { 0 , 1 } ) = 2 /\ m = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } ) -> ( m e/ Smgrp <-> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } e/ Smgrp ) ) with typecode |-
27	5 18 22	mgm2nsgrplem4	Could not format ( ( # ` { 0 , 1 } ) = 2 -> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } e/ Smgrp ) : No typesetting found for |- ( ( # ` { 0 , 1 } ) = 2 -> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } e/ Smgrp ) with typecode |-
28	24 26 27	rspcedvd	Could not format ( ( # ` { 0 , 1 } ) = 2 -> E. m e. Mgm m e/ Smgrp ) : No typesetting found for |- ( ( # ` { 0 , 1 } ) = 2 -> E. m e. Mgm m e/ Smgrp ) with typecode |-
29	1 28	ax-mp	Could not format E. m e. Mgm m e/ Smgrp : No typesetting found for |- E. m e. Mgm m e/ Smgrp with typecode |-