Theorem sgrp2nmndlem3

Description: Lemma 3 for sgrp2nmnd . (Contributed by AV, 29-Jan-2020)

	Ref	Expression
Hypotheses	mgm2nsgrp.s	$$⊢S=\left\{A,B\right\}$$
	mgm2nsgrp.b	$$⊢{\mathrm{Base}}_M=S$$
	sgrp2nmnd.o	$$⊢{+}_M=\left(x\in S,y\in S⟼if\left(x=A,A,B\right)\right)$$
	sgrp2nmnd.p	No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion	sgrp2nmndlem3	Could not format assertion : No typesetting found for |- ( ( C e. S /\ B e. S /\ A =/= B ) -> ( B .o. C ) = B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	$$⊢S=\left\{A,B\right\}$$
2		mgm2nsgrp.b	$$⊢{\mathrm{Base}}_M=S$$
3		sgrp2nmnd.o	$$⊢{+}_M=\left(x\in S,y\in S⟼if\left(x=A,A,B\right)\right)$$
4		sgrp2nmnd.p	Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |-
5	4 3	eqtri	Could not format .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) : No typesetting found for |- .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) with typecode |-
6	5	a1i	Could not format ( ( C e. S /\ B e. S /\ A =/= B ) -> .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) ) : No typesetting found for |- ( ( C e. S /\ B e. S /\ A =/= B ) -> .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) ) with typecode |-
7		df-ne	$$⊢A\ne B\leftrightarrow \neg A=B$$
8		eqeq2	$$⊢x=B\to \left(A=x\leftrightarrow A=B\right)$$
9	8	adantr	$$⊢\left(x=B\wedge y=C\right)\to \left(A=x\leftrightarrow A=B\right)$$
10		eqcom	$$⊢A=x\leftrightarrow x=A$$
11	9 10	bitr3di	$$⊢\left(x=B\wedge y=C\right)\to \left(A=B\leftrightarrow x=A\right)$$
12	11	notbid	$$⊢\left(x=B\wedge y=C\right)\to \left(\neg A=B\leftrightarrow \neg x=A\right)$$
13	12	biimpcd	$$⊢\neg A=B\to \left(\left(x=B\wedge y=C\right)\to \neg x=A\right)$$
14	7 13	sylbi	$$⊢A\ne B\to \left(\left(x=B\wedge y=C\right)\to \neg x=A\right)$$
15	14	3ad2ant3	$$⊢\left(C\in S\wedge B\in S\wedge A\ne B\right)\to \left(\left(x=B\wedge y=C\right)\to \neg x=A\right)$$
16	15	imp	$$⊢\left(\left(C\in S\wedge B\in S\wedge A\ne B\right)\wedge \left(x=B\wedge y=C\right)\right)\to \neg x=A$$
17	16	iffalsed	$$⊢\left(\left(C\in S\wedge B\in S\wedge A\ne B\right)\wedge \left(x=B\wedge y=C\right)\right)\to if\left(x=A,A,B\right)=B$$
18		simp2	$$⊢\left(C\in S\wedge B\in S\wedge A\ne B\right)\to B\in S$$
19		simp1	$$⊢\left(C\in S\wedge B\in S\wedge A\ne B\right)\to C\in S$$
20	6 17 18 19 18	ovmpod	Could not format ( ( C e. S /\ B e. S /\ A =/= B ) -> ( B .o. C ) = B ) : No typesetting found for |- ( ( C e. S /\ B e. S /\ A =/= B ) -> ( B .o. C ) = B ) with typecode |-