Theorem issgrpv

Description: The predicate "is a semigroup" for a structure which is a set. (Contributed by AV, 1-Feb-2020)

	Ref	Expression
Hypotheses	issgrpn0.b	$$⊢B={\mathrm{Base}}_M$$
	issgrpn0.o	No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion	issgrpv	Could not format assertion : No typesetting found for |- ( M e. V -> ( M e. Smgrp <-> A. x e. B A. y e. B ( ( x .o. y ) e. B /\ A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) ) 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	1 2	ismgm	Could not format ( M e. V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) : No typesetting found for |- ( M e. V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-
4	3	anbi1d	Could not format ( M e. V -> ( ( 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 ) ) ) <-> ( A. x e. B A. y e. B ( x .o. y ) e. B /\ 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. V -> ( ( 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 ) ) ) <-> ( A. x e. B A. y e. B ( x .o. y ) e. B /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) ) with typecode |-
5	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 |-
6		r19.26-2	Could not format ( A. x e. B A. y e. B ( ( x .o. 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 ( x .o. y ) e. B /\ 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 |- ( A. x e. B A. y e. B ( ( x .o. 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 ( x .o. y ) e. B /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |-
7	4 5 6	3bitr4g	Could not format ( M e. V -> ( M e. Smgrp <-> A. x e. B A. y e. B ( ( x .o. y ) e. B /\ A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) ) : No typesetting found for |- ( M e. V -> ( M e. Smgrp <-> A. x e. B A. y e. B ( ( x .o. y ) e. B /\ A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) ) with typecode |-