Theorem sgrpnmndex

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

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

Proof

Step	Hyp	Ref	Expression
1		prhash2ex	$$⊢\left|\left\{0,1\right\}\right|=2$$
2		eqid	$$⊢\left\{0,1\right\}=\left\{0,1\right\}$$
3		prex	$$⊢\left\{0,1\right\}\in \mathrm{V}$$
4		eqeq1	$$⊢x=u\to \left(x=0\leftrightarrow u=0\right)$$
5	4	ifbid	$$⊢x=u\to if\left(x=0,0,1\right)=if\left(u=0,0,1\right)$$
6		eqidd	$$⊢y=v\to if\left(u=0,0,1\right)=if\left(u=0,0,1\right)$$
7	5 6	cbvmpov	$$⊢\left(x\in \left\{0,1\right\},y\in \left\{0,1\right\}⟼if\left(x=0,0,1\right)\right)=\left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(u=0,0,1\right)\right)$$
8	7	opeq2i	$$⊢⟨{+}_{\mathrm{ndx}},\left(x\in \left\{0,1\right\},y\in \left\{0,1\right\}⟼if\left(x=0,0,1\right)\right)⟩=⟨{+}_{\mathrm{ndx}},\left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(u=0,0,1\right)\right)⟩$$
9	8	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(x=0,0,1\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(u=0,0,1\right)\right)⟩\right\}$$
10	9	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(x=0,0,1\right)\right)⟩\right\}}$$
11	3 10	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(x=0,0,1\right)\right)⟩\right\}}$$
12	11	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(x=0,0,1\right)\right)⟩\right\}}=\left\{0,1\right\}$$
13	3 3	mpoex	$$⊢\left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(u=0,0,1\right)\right)\in \mathrm{V}$$
14	9	grpplusg	$$⊢\left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(u=0,0,1\right)\right)\in \mathrm{V}\to \left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(u=0,0,1\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(x=0,0,1\right)\right)⟩\right\}}$$
15	13 14	ax-mp	$$⊢\left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(u=0,0,1\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(x=0,0,1\right)\right)⟩\right\}}$$
16	15	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(x=0,0,1\right)\right)⟩\right\}}=\left(u\in \left\{0,1\right\},v\in \left\{0,1\right\}⟼if\left(u=0,0,1\right)\right)$$
17	2 12 16	sgrp2nmndlem4	Could not format ( ( # ` { 0 , 1 } ) = 2 -> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } 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 , 0 , 1 ) ) >. } e. Smgrp ) with typecode |-
18		neleq1	$$⊢m=\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(x=0,0,1\right)\right)⟩\right\}\to \left(m\notin \mathrm{Mnd}\leftrightarrow \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(x=0,0,1\right)\right)⟩\right\}\notin \mathrm{Mnd}\right)$$
19	18	adantl	$$⊢\left(\left|\left\{0,1\right\}\right|=2\wedge m=\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(x=0,0,1\right)\right)⟩\right\}\right)\to \left(m\notin \mathrm{Mnd}\leftrightarrow \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(x=0,0,1\right)\right)⟩\right\}\notin \mathrm{Mnd}\right)$$
20	2 12 16	sgrp2nmndlem5	$$⊢\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(x=0,0,1\right)\right)⟩\right\}\notin \mathrm{Mnd}$$
21	17 19 20	rspcedvd	Could not format ( ( # ` { 0 , 1 } ) = 2 -> E. m e. Smgrp m e/ Mnd ) : No typesetting found for |- ( ( # ` { 0 , 1 } ) = 2 -> E. m e. Smgrp m e/ Mnd ) with typecode |-
22	1 21	ax-mp	Could not format E. m e. Smgrp m e/ Mnd : No typesetting found for |- E. m e. Smgrp m e/ Mnd with typecode |-