Theorem sgrp2rid2

Description: A small semigroup (with two elements) with two right identities which are different if A =/= B . (Contributed by AV, 10-Feb-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	sgrp2rid2	Could not format assertion : No typesetting found for |- ( ( A e. V /\ B e. W ) -> A. x e. S A. y e. S ( y .o. x ) = y ) 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		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		simpl	$$⊢\left(A\in S\wedge B\in S\right)\to A\in S$$
10	1 2 3 4	sgrp2nmndlem2	Could not format ( ( A e. S /\ A e. S ) -> ( A .o. A ) = A ) : No typesetting found for |- ( ( A e. S /\ A e. S ) -> ( A .o. A ) = A ) with typecode |-
11	9 10	syldan	Could not format ( ( A e. S /\ B e. S ) -> ( A .o. A ) = A ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> ( A .o. A ) = A ) with typecode |-
12		oveq1	Could not format ( A = B -> ( A .o. A ) = ( B .o. A ) ) : No typesetting found for |- ( A = B -> ( A .o. A ) = ( B .o. A ) ) with typecode |-
13		id	$$⊢A=B\to A=B$$
14	12 13	eqeq12d	Could not format ( A = B -> ( ( A .o. A ) = A <-> ( B .o. A ) = B ) ) : No typesetting found for |- ( A = B -> ( ( A .o. A ) = A <-> ( B .o. A ) = B ) ) with typecode |-
15	11 14	syl5ib	Could not format ( A = B -> ( ( A e. S /\ B e. S ) -> ( B .o. A ) = B ) ) : No typesetting found for |- ( A = B -> ( ( A e. S /\ B e. S ) -> ( B .o. A ) = B ) ) with typecode |-
16		simprl	$$⊢\left(\neg A=B\wedge \left(A\in S\wedge B\in S\right)\right)\to A\in S$$
17		simprr	$$⊢\left(\neg A=B\wedge \left(A\in S\wedge B\in S\right)\right)\to B\in S$$
18		neqne	$$⊢\neg A=B\to A\ne B$$
19	18	adantr	$$⊢\left(\neg A=B\wedge \left(A\in S\wedge B\in S\right)\right)\to A\ne B$$
20	1 2 3 4	sgrp2nmndlem3	Could not format ( ( A e. S /\ B e. S /\ A =/= B ) -> ( B .o. A ) = B ) : No typesetting found for |- ( ( A e. S /\ B e. S /\ A =/= B ) -> ( B .o. A ) = B ) with typecode |-
21	16 17 19 20	syl3anc	Could not format ( ( -. A = B /\ ( A e. S /\ B e. S ) ) -> ( B .o. A ) = B ) : No typesetting found for |- ( ( -. A = B /\ ( A e. S /\ B e. S ) ) -> ( B .o. A ) = B ) with typecode |-
22	21	ex	Could not format ( -. A = B -> ( ( A e. S /\ B e. S ) -> ( B .o. A ) = B ) ) : No typesetting found for |- ( -. A = B -> ( ( A e. S /\ B e. S ) -> ( B .o. A ) = B ) ) with typecode |-
23	15 22	pm2.61i	Could not format ( ( A e. S /\ B e. S ) -> ( B .o. A ) = B ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> ( B .o. A ) = B ) with typecode |-
24	1 2 3 4	sgrp2nmndlem2	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 |-
25	13 13	oveq12d	Could not format ( A = B -> ( A .o. A ) = ( B .o. B ) ) : No typesetting found for |- ( A = B -> ( A .o. A ) = ( B .o. B ) ) with typecode |-
26	25 13	eqeq12d	Could not format ( A = B -> ( ( A .o. A ) = A <-> ( B .o. B ) = B ) ) : No typesetting found for |- ( A = B -> ( ( A .o. A ) = A <-> ( B .o. B ) = B ) ) with typecode |-
27	11 26	syl5ib	Could not format ( A = B -> ( ( A e. S /\ B e. S ) -> ( B .o. B ) = B ) ) : No typesetting found for |- ( A = B -> ( ( A e. S /\ B e. S ) -> ( B .o. B ) = B ) ) with typecode |-
28	1 2 3 4	sgrp2nmndlem3	Could not format ( ( B e. S /\ B e. S /\ A =/= B ) -> ( B .o. B ) = B ) : No typesetting found for |- ( ( B e. S /\ B e. S /\ A =/= B ) -> ( B .o. B ) = B ) with typecode |-
29	17 17 19 28	syl3anc	Could not format ( ( -. A = B /\ ( A e. S /\ B e. S ) ) -> ( B .o. B ) = B ) : No typesetting found for |- ( ( -. A = B /\ ( A e. S /\ B e. S ) ) -> ( B .o. B ) = B ) with typecode |-
30	29	ex	Could not format ( -. A = B -> ( ( A e. S /\ B e. S ) -> ( B .o. B ) = B ) ) : No typesetting found for |- ( -. A = B -> ( ( A e. S /\ B e. S ) -> ( B .o. B ) = B ) ) with typecode |-
31	27 30	pm2.61i	Could not format ( ( A e. S /\ B e. S ) -> ( B .o. B ) = B ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> ( B .o. B ) = B ) with typecode |-
32	24 31	jca	Could not format ( ( A e. S /\ B e. S ) -> ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) with typecode |-
33	11 23 32	jca31	Could not format ( ( A e. S /\ B e. S ) -> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) with typecode |-
34	6 8 33	syl2an	Could not format ( ( A e. V /\ B e. W ) -> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) : No typesetting found for |- ( ( A e. V /\ B e. W ) -> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) with typecode |-
35	1	raleqi	Could not format ( A. y e. S ( y .o. x ) = y <-> A. y e. { A , B } ( y .o. x ) = y ) : No typesetting found for |- ( A. y e. S ( y .o. x ) = y <-> A. y e. { A , B } ( y .o. x ) = y ) with typecode |-
36		oveq1	Could not format ( y = A -> ( y .o. x ) = ( A .o. x ) ) : No typesetting found for |- ( y = A -> ( y .o. x ) = ( A .o. x ) ) with typecode |-
37		id	$$⊢y=A\to y=A$$
38	36 37	eqeq12d	Could not format ( y = A -> ( ( y .o. x ) = y <-> ( A .o. x ) = A ) ) : No typesetting found for |- ( y = A -> ( ( y .o. x ) = y <-> ( A .o. x ) = A ) ) with typecode |-
39		oveq1	Could not format ( y = B -> ( y .o. x ) = ( B .o. x ) ) : No typesetting found for |- ( y = B -> ( y .o. x ) = ( B .o. x ) ) with typecode |-
40		id	$$⊢y=B\to y=B$$
41	39 40	eqeq12d	Could not format ( y = B -> ( ( y .o. x ) = y <-> ( B .o. x ) = B ) ) : No typesetting found for |- ( y = B -> ( ( y .o. x ) = y <-> ( B .o. x ) = B ) ) with typecode |-
42	38 41	ralprg	Could not format ( ( A e. V /\ B e. W ) -> ( A. y e. { A , B } ( y .o. x ) = y <-> ( ( A .o. x ) = A /\ ( B .o. x ) = B ) ) ) : No typesetting found for |- ( ( A e. V /\ B e. W ) -> ( A. y e. { A , B } ( y .o. x ) = y <-> ( ( A .o. x ) = A /\ ( B .o. x ) = B ) ) ) with typecode |-
43	35 42	syl5bb	Could not format ( ( A e. V /\ B e. W ) -> ( A. y e. S ( y .o. x ) = y <-> ( ( A .o. x ) = A /\ ( B .o. x ) = B ) ) ) : No typesetting found for |- ( ( A e. V /\ B e. W ) -> ( A. y e. S ( y .o. x ) = y <-> ( ( A .o. x ) = A /\ ( B .o. x ) = B ) ) ) with typecode |-
44	43	ralbidv	Could not format ( ( A e. V /\ B e. W ) -> ( A. x e. S A. y e. S ( y .o. x ) = y <-> A. x e. S ( ( A .o. x ) = A /\ ( B .o. x ) = B ) ) ) : No typesetting found for |- ( ( A e. V /\ B e. W ) -> ( A. x e. S A. y e. S ( y .o. x ) = y <-> A. x e. S ( ( A .o. x ) = A /\ ( B .o. x ) = B ) ) ) with typecode |-
45	1	raleqi	Could not format ( A. x e. S ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> A. x e. { A , B } ( ( A .o. x ) = A /\ ( B .o. x ) = B ) ) : No typesetting found for |- ( A. x e. S ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> A. x e. { A , B } ( ( A .o. x ) = A /\ ( B .o. x ) = B ) ) with typecode |-
46		oveq2	Could not format ( x = A -> ( A .o. x ) = ( A .o. A ) ) : No typesetting found for |- ( x = A -> ( A .o. x ) = ( A .o. A ) ) with typecode |-
47	46	eqeq1d	Could not format ( x = A -> ( ( A .o. x ) = A <-> ( A .o. A ) = A ) ) : No typesetting found for |- ( x = A -> ( ( A .o. x ) = A <-> ( A .o. A ) = A ) ) with typecode |-
48		oveq2	Could not format ( x = A -> ( B .o. x ) = ( B .o. A ) ) : No typesetting found for |- ( x = A -> ( B .o. x ) = ( B .o. A ) ) with typecode |-
49	48	eqeq1d	Could not format ( x = A -> ( ( B .o. x ) = B <-> ( B .o. A ) = B ) ) : No typesetting found for |- ( x = A -> ( ( B .o. x ) = B <-> ( B .o. A ) = B ) ) with typecode |-
50	47 49	anbi12d	Could not format ( x = A -> ( ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> ( ( A .o. A ) = A /\ ( B .o. A ) = B ) ) ) : No typesetting found for |- ( x = A -> ( ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> ( ( A .o. A ) = A /\ ( B .o. A ) = B ) ) ) with typecode |-
51		oveq2	Could not format ( x = B -> ( A .o. x ) = ( A .o. B ) ) : No typesetting found for |- ( x = B -> ( A .o. x ) = ( A .o. B ) ) with typecode |-
52	51	eqeq1d	Could not format ( x = B -> ( ( A .o. x ) = A <-> ( A .o. B ) = A ) ) : No typesetting found for |- ( x = B -> ( ( A .o. x ) = A <-> ( A .o. B ) = A ) ) with typecode |-
53		oveq2	Could not format ( x = B -> ( B .o. x ) = ( B .o. B ) ) : No typesetting found for |- ( x = B -> ( B .o. x ) = ( B .o. B ) ) with typecode |-
54	53	eqeq1d	Could not format ( x = B -> ( ( B .o. x ) = B <-> ( B .o. B ) = B ) ) : No typesetting found for |- ( x = B -> ( ( B .o. x ) = B <-> ( B .o. B ) = B ) ) with typecode |-
55	52 54	anbi12d	Could not format ( x = B -> ( ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) : No typesetting found for |- ( x = B -> ( ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) with typecode |-
56	50 55	ralprg	Could not format ( ( A e. V /\ B e. W ) -> ( A. x e. { A , B } ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) ) : No typesetting found for |- ( ( A e. V /\ B e. W ) -> ( A. x e. { A , B } ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) ) with typecode |-
57	45 56	syl5bb	Could not format ( ( A e. V /\ B e. W ) -> ( A. x e. S ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) ) : No typesetting found for |- ( ( A e. V /\ B e. W ) -> ( A. x e. S ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) ) with typecode |-
58	44 57	bitrd	Could not format ( ( A e. V /\ B e. W ) -> ( A. x e. S A. y e. S ( y .o. x ) = y <-> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) ) : No typesetting found for |- ( ( A e. V /\ B e. W ) -> ( A. x e. S A. y e. S ( y .o. x ) = y <-> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) ) with typecode |-
59	34 58	mpbird	Could not format ( ( A e. V /\ B e. W ) -> A. x e. S A. y e. S ( y .o. x ) = y ) : No typesetting found for |- ( ( A e. V /\ B e. W ) -> A. x e. S A. y e. S ( y .o. x ) = y ) with typecode |-