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=\left\{A,B\right\}$$
	mgm2nsgrp.b	$$⊢{\mathrm{Base}}_M=S$$
	mgm2nsgrp.o	$$⊢{+}_M=\left(x\in S,y\in S⟼if\left(\left(x=A\wedge y=A\right),B,A\right)\right)$$
Assertion	mgm2nsgrplem1	$$⊢\left(A\in V\wedge B\in W\right)\to M\in \mathrm{Mgm}$$

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	$$⊢S=\left\{A,B\right\}$$
2		mgm2nsgrp.b	$$⊢{\mathrm{Base}}_M=S$$
3		mgm2nsgrp.o	$$⊢{+}_M=\left(x\in S,y\in S⟼if\left(\left(x=A\wedge y=A\right),B,A\right)\right)$$
4		prid1g	$$⊢A\in V\to A\in \left\{A,B\right\}$$
5	4 1	eleqtrrdi	$$⊢A\in V\to A\in S$$
6		prid2g	$$⊢B\in W\to B\in \left\{A,B\right\}$$
7	6 1	eleqtrrdi	$$⊢B\in W\to B\in S$$
8	2	eqcomi	$$⊢S={\mathrm{Base}}_M$$
9		ne0i	$$⊢A\in S\to S\ne \varnothing$$
10	9	adantr	$$⊢\left(A\in S\wedge B\in S\right)\to S\ne \varnothing$$
11		simplr	$$⊢\left(\left(A\in S\wedge B\in S\right)\wedge \left(x\in S\wedge y\in S\right)\right)\to B\in S$$
12		simpll	$$⊢\left(\left(A\in S\wedge B\in S\right)\wedge \left(x\in S\wedge y\in S\right)\right)\to A\in S$$
13	8 3 10 11 12	opifismgm	$$⊢\left(A\in S\wedge B\in S\right)\to M\in \mathrm{Mgm}$$
14	5 7 13	syl2an	$$⊢\left(A\in V\wedge B\in W\right)\to M\in \mathrm{Mgm}$$