Theorem mgm2nsgrplem3

Description: Lemma 3 for mgm2nsgrp . (Contributed by AV, 28-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	mgm2nsgrplem3	Could not format assertion : No typesetting found for |- ( ( A e. V /\ B e. W ) -> ( A .o. ( A .o. B ) ) = B ) 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		simprl	Could not format ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = ( A .o. B ) ) ) -> x = A ) : No typesetting found for |- ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = ( A .o. B ) ) ) -> x = A ) with typecode |-
12		simpr	Could not format ( ( x = A /\ y = ( A .o. B ) ) -> y = ( A .o. B ) ) : No typesetting found for |- ( ( x = A /\ y = ( A .o. B ) ) -> y = ( A .o. B ) ) with typecode |-
13		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)$$
14		ifid	$$⊢if\left(\left(x=A\wedge y=A\right),A,A\right)=A$$
15	13 14	eqtrdi	$$⊢B=A\to if\left(\left(x=A\wedge y=A\right),B,A\right)=A$$
16	15	a1d	$$⊢B=A\to \left(\left(x=A\wedge y=B\right)\to if\left(\left(x=A\wedge y=A\right),B,A\right)=A\right)$$
17		eqeq1	$$⊢y=B\to \left(y=A\leftrightarrow B=A\right)$$
18	17	biimpcd	$$⊢y=A\to \left(y=B\to B=A\right)$$
19	18	adantl	$$⊢\left(x=A\wedge y=A\right)\to \left(y=B\to B=A\right)$$
20	19	com12	$$⊢y=B\to \left(\left(x=A\wedge y=A\right)\to B=A\right)$$
21	20	adantl	$$⊢\left(x=A\wedge y=B\right)\to \left(\left(x=A\wedge y=A\right)\to B=A\right)$$
22	21	con3d	$$⊢\left(x=A\wedge y=B\right)\to \left(\neg B=A\to \neg \left(x=A\wedge y=A\right)\right)$$
23	22	impcom	$$⊢\left(\neg B=A\wedge \left(x=A\wedge y=B\right)\right)\to \neg \left(x=A\wedge y=A\right)$$
24	23	iffalsed	$$⊢\left(\neg B=A\wedge \left(x=A\wedge y=B\right)\right)\to if\left(\left(x=A\wedge y=A\right),B,A\right)=A$$
25	24	ex	$$⊢\neg B=A\to \left(\left(x=A\wedge y=B\right)\to if\left(\left(x=A\wedge y=A\right),B,A\right)=A\right)$$
26	16 25	pm2.61i	$$⊢\left(x=A\wedge y=B\right)\to if\left(\left(x=A\wedge y=A\right),B,A\right)=A$$
27	26	adantl	$$⊢\left(\left(A\in S\wedge B\in S\right)\wedge \left(x=A\wedge y=B\right)\right)\to if\left(\left(x=A\wedge y=A\right),B,A\right)=A$$
28		simpl	$$⊢\left(A\in S\wedge B\in S\right)\to A\in S$$
29		simpr	$$⊢\left(A\in S\wedge B\in S\right)\to B\in S$$
30	10 27 28 29 28	ovmpod	Could not format ( ( A e. S /\ B e. S ) -> ( A .o. B ) = A ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> ( A .o. B ) = A ) with typecode |-
31	12 30	sylan9eqr	Could not format ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = ( A .o. B ) ) ) -> y = A ) : No typesetting found for |- ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = ( A .o. B ) ) ) -> y = A ) with typecode |-
32	11 31	jca	Could not format ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = ( A .o. B ) ) ) -> ( x = A /\ y = A ) ) : No typesetting found for |- ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = ( A .o. B ) ) ) -> ( x = A /\ y = A ) ) with typecode |-
33	32	iftrued	Could not format ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = ( A .o. B ) ) ) -> if ( ( x = A /\ y = A ) , B , A ) = B ) : No typesetting found for |- ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = ( A .o. B ) ) ) -> if ( ( x = A /\ y = A ) , B , A ) = B ) with typecode |-
34	30 28	eqeltrd	Could not format ( ( A e. S /\ B e. S ) -> ( A .o. B ) e. S ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> ( A .o. B ) e. S ) with typecode |-
35	10 33 28 34 29	ovmpod	Could not format ( ( A e. S /\ B e. S ) -> ( A .o. ( A .o. B ) ) = B ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> ( A .o. ( A .o. B ) ) = B ) with typecode |-
36	6 8 35	syl2an	Could not format ( ( A e. V /\ B e. W ) -> ( A .o. ( A .o. B ) ) = B ) : No typesetting found for |- ( ( A e. V /\ B e. W ) -> ( A .o. ( A .o. B ) ) = B ) with typecode |-