Theorem sgrp2rid2ex

Description: A small semigroup (with two elements) with two right identities which are different. (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	sgrp2rid2ex	Could not format assertion : No typesetting found for |- ( ( # ` S ) = 2 -> E. x e. S E. z e. S A. y e. S ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = 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	1	hashprdifel	$$⊢\left|S\right|=2\to \left(A\in S\wedge B\in S\wedge A\ne B\right)$$
6		simp1	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to A\in S$$
7		simp2	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to B\in S$$
8		simpl3	$$⊢\left(\left(A\in S\wedge B\in S\wedge A\ne B\right)\wedge y\in S\right)\to A\ne B$$
9	8	ralrimiva	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \forall y\in SA\ne B$$
10	1 2 3 4	sgrp2rid2	Could not format ( ( A e. S /\ B e. S ) -> A. x e. S A. y e. S ( y .o. x ) = y ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> A. x e. S A. y e. S ( y .o. x ) = y ) with typecode |-
11		oveq2	Could not format ( x = A -> ( y .o. x ) = ( y .o. A ) ) : No typesetting found for |- ( x = A -> ( y .o. x ) = ( y .o. A ) ) with typecode |-
12	11	eqeq1d	Could not format ( x = A -> ( ( y .o. x ) = y <-> ( y .o. A ) = y ) ) : No typesetting found for |- ( x = A -> ( ( y .o. x ) = y <-> ( y .o. A ) = y ) ) with typecode |-
13	12	ralbidv	Could not format ( x = A -> ( A. y e. S ( y .o. x ) = y <-> A. y e. S ( y .o. A ) = y ) ) : No typesetting found for |- ( x = A -> ( A. y e. S ( y .o. x ) = y <-> A. y e. S ( y .o. A ) = y ) ) with typecode |-
14	13	rspcv	Could not format ( A e. S -> ( A. x e. S A. y e. S ( y .o. x ) = y -> A. y e. S ( y .o. A ) = y ) ) : No typesetting found for |- ( A e. S -> ( A. x e. S A. y e. S ( y .o. x ) = y -> A. y e. S ( y .o. A ) = y ) ) with typecode |-
15	14	adantr	Could not format ( ( A e. S /\ B e. S ) -> ( A. x e. S A. y e. S ( y .o. x ) = y -> A. y e. S ( y .o. A ) = y ) ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> ( A. x e. S A. y e. S ( y .o. x ) = y -> A. y e. S ( y .o. A ) = y ) ) with typecode |-
16	10 15	mpd	Could not format ( ( A e. S /\ B e. S ) -> A. y e. S ( y .o. A ) = y ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> A. y e. S ( y .o. A ) = y ) with typecode |-
17	16	3adant3	Could not format ( ( A e. S /\ B e. S /\ A =/= B ) -> A. y e. S ( y .o. A ) = y ) : No typesetting found for |- ( ( A e. S /\ B e. S /\ A =/= B ) -> A. y e. S ( y .o. A ) = y ) with typecode |-
18		oveq2	Could not format ( x = B -> ( y .o. x ) = ( y .o. B ) ) : No typesetting found for |- ( x = B -> ( y .o. x ) = ( y .o. B ) ) with typecode |-
19	18	eqeq1d	Could not format ( x = B -> ( ( y .o. x ) = y <-> ( y .o. B ) = y ) ) : No typesetting found for |- ( x = B -> ( ( y .o. x ) = y <-> ( y .o. B ) = y ) ) with typecode |-
20	19	ralbidv	Could not format ( x = B -> ( A. y e. S ( y .o. x ) = y <-> A. y e. S ( y .o. B ) = y ) ) : No typesetting found for |- ( x = B -> ( A. y e. S ( y .o. x ) = y <-> A. y e. S ( y .o. B ) = y ) ) with typecode |-
21	20	rspcv	Could not format ( B e. S -> ( A. x e. S A. y e. S ( y .o. x ) = y -> A. y e. S ( y .o. B ) = y ) ) : No typesetting found for |- ( B e. S -> ( A. x e. S A. y e. S ( y .o. x ) = y -> A. y e. S ( y .o. B ) = y ) ) with typecode |-
22	21	adantl	Could not format ( ( A e. S /\ B e. S ) -> ( A. x e. S A. y e. S ( y .o. x ) = y -> A. y e. S ( y .o. B ) = y ) ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> ( A. x e. S A. y e. S ( y .o. x ) = y -> A. y e. S ( y .o. B ) = y ) ) with typecode |-
23	10 22	mpd	Could not format ( ( A e. S /\ B e. S ) -> A. y e. S ( y .o. B ) = y ) : No typesetting found for |- ( ( A e. S /\ B e. S ) -> A. y e. S ( y .o. B ) = y ) with typecode |-
24	23	3adant3	Could not format ( ( A e. S /\ B e. S /\ A =/= B ) -> A. y e. S ( y .o. B ) = y ) : No typesetting found for |- ( ( A e. S /\ B e. S /\ A =/= B ) -> A. y e. S ( y .o. B ) = y ) with typecode |-
25		r19.26-3	Could not format ( A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) <-> ( A. y e. S A =/= B /\ A. y e. S ( y .o. A ) = y /\ A. y e. S ( y .o. B ) = y ) ) : No typesetting found for |- ( A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) <-> ( A. y e. S A =/= B /\ A. y e. S ( y .o. A ) = y /\ A. y e. S ( y .o. B ) = y ) ) with typecode |-
26	9 17 24 25	syl3anbrc	Could not format ( ( A e. S /\ B e. S /\ A =/= B ) -> A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) : No typesetting found for |- ( ( A e. S /\ B e. S /\ A =/= B ) -> A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) with typecode |-
27	6 7 26	3jca	Could not format ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A e. S /\ B e. S /\ A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) ) : No typesetting found for |- ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A e. S /\ B e. S /\ A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) ) with typecode |-
28		neeq1	$$⊢x=A\to \left(x\ne z\leftrightarrow A\ne z\right)$$
29		biidd	Could not format ( x = A -> ( ( y .o. z ) = y <-> ( y .o. z ) = y ) ) : No typesetting found for |- ( x = A -> ( ( y .o. z ) = y <-> ( y .o. z ) = y ) ) with typecode |-
30	28 12 29	3anbi123d	Could not format ( x = A -> ( ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = y ) <-> ( A =/= z /\ ( y .o. A ) = y /\ ( y .o. z ) = y ) ) ) : No typesetting found for |- ( x = A -> ( ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = y ) <-> ( A =/= z /\ ( y .o. A ) = y /\ ( y .o. z ) = y ) ) ) with typecode |-
31	30	ralbidv	Could not format ( x = A -> ( A. y e. S ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = y ) <-> A. y e. S ( A =/= z /\ ( y .o. A ) = y /\ ( y .o. z ) = y ) ) ) : No typesetting found for |- ( x = A -> ( A. y e. S ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = y ) <-> A. y e. S ( A =/= z /\ ( y .o. A ) = y /\ ( y .o. z ) = y ) ) ) with typecode |-
32		neeq2	$$⊢z=B\to \left(A\ne z\leftrightarrow A\ne B\right)$$
33		biidd	Could not format ( z = B -> ( ( y .o. A ) = y <-> ( y .o. A ) = y ) ) : No typesetting found for |- ( z = B -> ( ( y .o. A ) = y <-> ( y .o. A ) = y ) ) with typecode |-
34		oveq2	Could not format ( z = B -> ( y .o. z ) = ( y .o. B ) ) : No typesetting found for |- ( z = B -> ( y .o. z ) = ( y .o. B ) ) with typecode |-
35	34	eqeq1d	Could not format ( z = B -> ( ( y .o. z ) = y <-> ( y .o. B ) = y ) ) : No typesetting found for |- ( z = B -> ( ( y .o. z ) = y <-> ( y .o. B ) = y ) ) with typecode |-
36	32 33 35	3anbi123d	Could not format ( z = B -> ( ( A =/= z /\ ( y .o. A ) = y /\ ( y .o. z ) = y ) <-> ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) ) : No typesetting found for |- ( z = B -> ( ( A =/= z /\ ( y .o. A ) = y /\ ( y .o. z ) = y ) <-> ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) ) with typecode |-
37	36	ralbidv	Could not format ( z = B -> ( A. y e. S ( A =/= z /\ ( y .o. A ) = y /\ ( y .o. z ) = y ) <-> A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) ) : No typesetting found for |- ( z = B -> ( A. y e. S ( A =/= z /\ ( y .o. A ) = y /\ ( y .o. z ) = y ) <-> A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) ) with typecode |-
38	31 37	rspc2ev	Could not format ( ( A e. S /\ B e. S /\ A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) -> E. x e. S E. z e. S A. y e. S ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = y ) ) : No typesetting found for |- ( ( A e. S /\ B e. S /\ A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) -> E. x e. S E. z e. S A. y e. S ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = y ) ) with typecode |-
39	5 27 38	3syl	Could not format ( ( # ` S ) = 2 -> E. x e. S E. z e. S A. y e. S ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = y ) ) : No typesetting found for |- ( ( # ` S ) = 2 -> E. x e. S E. z e. S A. y e. S ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = y ) ) with typecode |-