Theorem isnsgrp

Description: A condition for a structure not to be a semigroup. (Contributed by AV, 30-Jan-2020)

	Ref	Expression
Hypotheses	issgrpn0.b	$$⊢B={\mathrm{Base}}_M$$
	issgrpn0.o	No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion	isnsgrp	Could not format assertion : No typesetting found for |- ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> M e/ Smgrp ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		issgrpn0.b	$$⊢B={\mathrm{Base}}_M$$
2		issgrpn0.o	Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |-
3		simpl1	Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> X e. B ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> X e. B ) with typecode |-
4		oveq1	Could not format ( x = X -> ( x .o. y ) = ( X .o. y ) ) : No typesetting found for |- ( x = X -> ( x .o. y ) = ( X .o. y ) ) with typecode |-
5	4	oveq1d	Could not format ( x = X -> ( ( x .o. y ) .o. z ) = ( ( X .o. y ) .o. z ) ) : No typesetting found for |- ( x = X -> ( ( x .o. y ) .o. z ) = ( ( X .o. y ) .o. z ) ) with typecode |-
6		oveq1	Could not format ( x = X -> ( x .o. ( y .o. z ) ) = ( X .o. ( y .o. z ) ) ) : No typesetting found for |- ( x = X -> ( x .o. ( y .o. z ) ) = ( X .o. ( y .o. z ) ) ) with typecode |-
7	5 6	eqeq12d	Could not format ( x = X -> ( ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( x = X -> ( ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) with typecode |-
8	7	notbid	Could not format ( x = X -> ( -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( x = X -> ( -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) with typecode |-
9	8	rexbidv	Could not format ( x = X -> ( E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( x = X -> ( E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) with typecode |-
10	9	rexbidv	Could not format ( x = X -> ( E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( x = X -> ( E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) with typecode |-
11	10	adantl	Could not format ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ x = X ) -> ( E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ x = X ) -> ( E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) with typecode |-
12		simpl2	Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> Y e. B ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> Y e. B ) with typecode |-
13		oveq2	Could not format ( y = Y -> ( X .o. y ) = ( X .o. Y ) ) : No typesetting found for |- ( y = Y -> ( X .o. y ) = ( X .o. Y ) ) with typecode |-
14	13	oveq1d	Could not format ( y = Y -> ( ( X .o. y ) .o. z ) = ( ( X .o. Y ) .o. z ) ) : No typesetting found for |- ( y = Y -> ( ( X .o. y ) .o. z ) = ( ( X .o. Y ) .o. z ) ) with typecode |-
15		oveq1	Could not format ( y = Y -> ( y .o. z ) = ( Y .o. z ) ) : No typesetting found for |- ( y = Y -> ( y .o. z ) = ( Y .o. z ) ) with typecode |-
16	15	oveq2d	Could not format ( y = Y -> ( X .o. ( y .o. z ) ) = ( X .o. ( Y .o. z ) ) ) : No typesetting found for |- ( y = Y -> ( X .o. ( y .o. z ) ) = ( X .o. ( Y .o. z ) ) ) with typecode |-
17	14 16	eqeq12d	Could not format ( y = Y -> ( ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) : No typesetting found for |- ( y = Y -> ( ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) with typecode |-
18	17	notbid	Could not format ( y = Y -> ( -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) : No typesetting found for |- ( y = Y -> ( -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) with typecode |-
19	18	adantl	Could not format ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ y = Y ) -> ( -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) : No typesetting found for |- ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ y = Y ) -> ( -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) with typecode |-
20	19	rexbidv	Could not format ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ y = Y ) -> ( E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> E. z e. B -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) : No typesetting found for |- ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ y = Y ) -> ( E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> E. z e. B -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) with typecode |-
21		simpl3	Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> Z e. B ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> Z e. B ) with typecode |-
22		oveq2	Could not format ( z = Z -> ( ( X .o. Y ) .o. z ) = ( ( X .o. Y ) .o. Z ) ) : No typesetting found for |- ( z = Z -> ( ( X .o. Y ) .o. z ) = ( ( X .o. Y ) .o. Z ) ) with typecode |-
23		oveq2	Could not format ( z = Z -> ( Y .o. z ) = ( Y .o. Z ) ) : No typesetting found for |- ( z = Z -> ( Y .o. z ) = ( Y .o. Z ) ) with typecode |-
24	23	oveq2d	Could not format ( z = Z -> ( X .o. ( Y .o. z ) ) = ( X .o. ( Y .o. Z ) ) ) : No typesetting found for |- ( z = Z -> ( X .o. ( Y .o. z ) ) = ( X .o. ( Y .o. Z ) ) ) with typecode |-
25	22 24	eqeq12d	Could not format ( z = Z -> ( ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) : No typesetting found for |- ( z = Z -> ( ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) with typecode |-
26	25	notbid	Could not format ( z = Z -> ( -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) : No typesetting found for |- ( z = Z -> ( -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) with typecode |-
27	26	adantl	Could not format ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ z = Z ) -> ( -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) : No typesetting found for |- ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ z = Z ) -> ( -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) with typecode |-
28		neneq	Could not format ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) : No typesetting found for |- ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) with typecode |-
29	28	adantl	Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) with typecode |-
30	21 27 29	rspcedvd	Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. z e. B -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. z e. B -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) with typecode |-
31	12 20 30	rspcedvd	Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) with typecode |-
32	3 11 31	rspcedvd	Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |-
33		rexnal	Could not format ( E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |-
34	33	2rexbii	Could not format ( E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. x e. B E. y e. B -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. x e. B E. y e. B -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |-
35		rexnal2	Could not format ( E. x e. B E. y e. B -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( E. x e. B E. y e. B -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |-
36	34 35	bitr2i	Could not format ( -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |-
37	32 36	sylibr	Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |-
38	37	intnand	Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |-
39	1 2	issgrp	Could not format ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |-
40	38 39	sylnibr	Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. M e. Smgrp ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. M e. Smgrp ) with typecode |-
41		df-nel	$$⊢M\notin \mathrm{Smgrp}\leftrightarrow \neg M\in \mathrm{Smgrp}$$
42	40 41	sylibr	Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> M e/ Smgrp ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> M e/ Smgrp ) with typecode |-
43	42	ex	Could not format ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> M e/ Smgrp ) ) : No typesetting found for |- ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> M e/ Smgrp ) ) with typecode |-