Theorem mgm2nsgrplem2

Description: Lemma 2 for mgm2nsgrp . (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)$$
	mgm2nsgrp.p	No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion	mgm2nsgrplem2	Could not format assertion : No typesetting found for |- ( ( A e. V /\ B e. W ) -> ( ( A .o. A ) .o. B ) = A ) with typecode |-

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		mgm2nsgrp.p	Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |-
5		prid1g	$$⊢A\in V\to A\in \left\{A,B\right\}$$
6	5 1	eleqtrrdi	$$⊢A\in V\to A\in S$$
7		prid2g	$$⊢B\in W\to B\in \left\{A,B\right\}$$
8	7 1	eleqtrrdi	$$⊢B\in W\to B\in S$$
9	4 3	eqtri	Could not format .o. = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) ) : No typesetting found for |- .o. = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) ) with typecode |-
10	9	a1i	Could not format ( ( A e. S /\ B e. S ) -> .o. = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) ) ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> .o. = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) ) ) with typecode |-
11		ifeq1	$$⊢B=A\to if\left(\left(x=A\wedge y=A\right),B,A\right)=if\left(\left(x=A\wedge y=A\right),A,A\right)$$
12		ifid	$$⊢if\left(\left(x=A\wedge y=A\right),A,A\right)=A$$
13	11 12	eqtrdi	$$⊢B=A\to if\left(\left(x=A\wedge y=A\right),B,A\right)=A$$
14	13	a1d	$$⊢B=A\to \left(y=B\to if\left(\left(x=A\wedge y=A\right),B,A\right)=A\right)$$
15		eqeq1	$$⊢y=B\to \left(y=A\leftrightarrow B=A\right)$$
16	15	bicomd	$$⊢y=B\to \left(B=A\leftrightarrow y=A\right)$$
17	16	notbid	$$⊢y=B\to \left(\neg B=A\leftrightarrow \neg y=A\right)$$
18	17	biimpac	$$⊢\left(\neg B=A\wedge y=B\right)\to \neg y=A$$
19	18	intnand	$$⊢\left(\neg B=A\wedge y=B\right)\to \neg \left(x=A\wedge y=A\right)$$
20	19	iffalsed	$$⊢\left(\neg B=A\wedge y=B\right)\to if\left(\left(x=A\wedge y=A\right),B,A\right)=A$$
21	20	ex	$$⊢\neg B=A\to \left(y=B\to if\left(\left(x=A\wedge y=A\right),B,A\right)=A\right)$$
22	14 21	pm2.61i	$$⊢y=B\to if\left(\left(x=A\wedge y=A\right),B,A\right)=A$$
23	22	ad2antll	Could not format ( ( ( A e. S /\ B e. S ) /\ ( x = ( A .o. A ) /\ y = B ) ) -> if ( ( x = A /\ y = A ) , B , A ) = A ) : No typesetting found for |- ( ( ( A e. S /\ B e. S ) /\ ( x = ( A .o. A ) /\ y = B ) ) -> if ( ( x = A /\ y = A ) , B , A ) = A ) with typecode |-
24		iftrue	$$⊢\left(x=A\wedge y=A\right)\to if\left(\left(x=A\wedge y=A\right),B,A\right)=B$$
25	24	adantl	$$⊢\left(\left(A\in S\wedge B\in S\right)\wedge \left(x=A\wedge y=A\right)\right)\to if\left(\left(x=A\wedge y=A\right),B,A\right)=B$$
26		simpl	$$⊢\left(A\in S\wedge B\in S\right)\to A\in S$$
27		simpr	$$⊢\left(A\in S\wedge B\in S\right)\to B\in S$$
28	10 25 26 26 27	ovmpod	Could not format ( ( A e. S /\ B e. S ) -> ( A .o. A ) = B ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> ( A .o. A ) = B ) with typecode |-
29	28 27	eqeltrd	Could not format ( ( A e. S /\ B e. S ) -> ( A .o. A ) e. S ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> ( A .o. A ) e. S ) with typecode |-
30	10 23 29 27 26	ovmpod	Could not format ( ( A e. S /\ B e. S ) -> ( ( A .o. A ) .o. B ) = A ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> ( ( A .o. A ) .o. B ) = A ) with typecode |-
31	6 8 30	syl2an	Could not format ( ( A e. V /\ B e. W ) -> ( ( A .o. A ) .o. B ) = A ) : No typesetting found for |- ( ( A e. V /\ B e. W ) -> ( ( A .o. A ) .o. B ) = A ) with typecode |-