Theorem sgrp2nmndlem1

Description: Lemma 1 for sgrp2nmnd : M is a magma, even if A = B ( M is the trivial magma in this case, see mgmb1mgm1 ). (Contributed by AV, 29-Jan-2020)

	Ref	Expression
Hypotheses	mgm2nsgrp.s	|- S = { A , B }
	mgm2nsgrp.b	|- ( Base ` M ) = S
	sgrp2nmnd.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )
Assertion	sgrp2nmndlem1	|- ( ( A e. V /\ B e. W ) -> M e. Mgm )

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	|- S = { A , B }
2		mgm2nsgrp.b	|- ( Base ` M ) = S
3		sgrp2nmnd.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )
4		prid1g	|- ( A e. V -> A e. { A , B } )
5	4 1	eleqtrrdi	|- ( A e. V -> A e. S )
6		prid2g	|- ( B e. W -> B e. { A , B } )
7	6 1	eleqtrrdi	|- ( B e. W -> B e. S )
8	2	eqcomi	|- S = ( Base ` M )
9		ne0i	|- ( A e. S -> S =/= (/) )
10	9	adantr	|- ( ( A e. S /\ B e. S ) -> S =/= (/) )
11		simpll	|- ( ( ( A e. S /\ B e. S ) /\ ( x e. S /\ y e. S ) ) -> A e. S )
12		simplr	|- ( ( ( A e. S /\ B e. S ) /\ ( x e. S /\ y e. S ) ) -> B e. S )
13	8 3 10 11 12	opifismgm	|- ( ( A e. S /\ B e. S ) -> M e. Mgm )
14	5 7 13	syl2an	|- ( ( A e. V /\ B e. W ) -> M e. Mgm )