Theorem mgm2nsgrplem1

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

	Ref	Expression
Hypotheses	mgm2nsgrp.s	|- S = { A , B }
	mgm2nsgrp.b	|- ( Base ` M ) = S
	mgm2nsgrp.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) )
Assertion	mgm2nsgrplem1	|- ( ( 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		mgm2nsgrp.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) )
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		simplr	|- ( ( ( A e. S /\ B e. S ) /\ ( x e. S /\ y e. S ) ) -> B e. S )
12		simpll	|- ( ( ( A e. S /\ B e. S ) /\ ( x e. S /\ y e. S ) ) -> A 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 )