Theorem sgrp2nmndlem2

Description: Lemma 2 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	sgrp2nmndlem2	Could not format assertion : No typesetting found for |- ( ( A e. S /\ C e. S ) -> ( A .o. C ) = A ) 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 ( ( A e. S /\ C e. S ) -> .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) ) : No typesetting found for |- ( ( A e. S /\ C e. S ) -> .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) ) with typecode |-
7		iftrue	$$⊢x=A\to if\left(x=A,A,B\right)=A$$
8	7	ad2antrl	$$⊢\left(\left(A\in S\wedge C\in S\right)\wedge \left(x=A\wedge y=C\right)\right)\to if\left(x=A,A,B\right)=A$$
9		simpl	$$⊢\left(A\in S\wedge C\in S\right)\to A\in S$$
10		simpr	$$⊢\left(A\in S\wedge C\in S\right)\to C\in S$$
11	6 8 9 10 9	ovmpod	Could not format ( ( A e. S /\ C e. S ) -> ( A .o. C ) = A ) : No typesetting found for |- ( ( A e. S /\ C e. S ) -> ( A .o. C ) = A ) with typecode |-