Theorem issgrpn0

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

	Ref	Expression
Hypotheses	issgrpn0.b	|- B = ( Base ` M )
	issgrpn0.o	|- .o. = ( +g ` M )
Assertion	issgrpn0	|- ( A e. B -> ( 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 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		issgrpn0.b	|- B = ( Base ` M )
2		issgrpn0.o	|- .o. = ( +g ` M )
3	1 2	ismgmn0	|- ( A e. B -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) )
4	3	anbi1d	|- ( A e. B -> ( ( 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 ) ) ) ) )
5	1 2	issgrp	|- ( 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 ) ) ) )
6		r19.26-2	|- ( 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 ) ) ) )
7	4 5 6	3bitr4g	|- ( A e. B -> ( 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 ) ) ) ) )