Theorem exidu1

Description: Obsolete theorem, use mgmidmo or mndideu instead. Uniqueness of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	exidu1.1	$$⊢X=\mathrm{ran}G$$
Assertion	exidu1	$$⊢G\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to \exists !u\in X\forall x\in X\left(uGx=x\wedge xGu=x\right)$$

Proof

Step	Hyp	Ref	Expression
1		exidu1.1	$$⊢X=\mathrm{ran}G$$
2	1	isexid2	$$⊢G\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to \exists u\in X\forall x\in X\left(uGx=x\wedge xGu=x\right)$$
3		simpl	$$⊢\left(uGx=x\wedge xGu=x\right)\to uGx=x$$
4	3	ralimi	$$⊢\forall x\in X\left(uGx=x\wedge xGu=x\right)\to \forall x\in XuGx=x$$
5		oveq2	$$⊢x=y\to uGx=uGy$$
6		id	$$⊢x=y\to x=y$$
7	5 6	eqeq12d	$$⊢x=y\to \left(uGx=x\leftrightarrow uGy=y\right)$$
8	7	rspcv	$$⊢y\in X\to \left(\forall x\in XuGx=x\to uGy=y\right)$$
9	4 8	syl5	$$⊢y\in X\to \left(\forall x\in X\left(uGx=x\wedge xGu=x\right)\to uGy=y\right)$$
10		simpr	$$⊢\left(yGx=x\wedge xGy=x\right)\to xGy=x$$
11	10	ralimi	$$⊢\forall x\in X\left(yGx=x\wedge xGy=x\right)\to \forall x\in XxGy=x$$
12		oveq1	$$⊢x=u\to xGy=uGy$$
13		id	$$⊢x=u\to x=u$$
14	12 13	eqeq12d	$$⊢x=u\to \left(xGy=x\leftrightarrow uGy=u\right)$$
15	14	rspcv	$$⊢u\in X\to \left(\forall x\in XxGy=x\to uGy=u\right)$$
16	11 15	syl5	$$⊢u\in X\to \left(\forall x\in X\left(yGx=x\wedge xGy=x\right)\to uGy=u\right)$$
17	9 16	im2anan9r	$$⊢\left(u\in X\wedge y\in X\right)\to \left(\left(\forall x\in X\left(uGx=x\wedge xGu=x\right)\wedge \forall x\in X\left(yGx=x\wedge xGy=x\right)\right)\to \left(uGy=y\wedge uGy=u\right)\right)$$
18		eqtr2	$$⊢\left(uGy=y\wedge uGy=u\right)\to y=u$$
19	18	equcomd	$$⊢\left(uGy=y\wedge uGy=u\right)\to u=y$$
20	17 19	syl6	$$⊢\left(u\in X\wedge y\in X\right)\to \left(\left(\forall x\in X\left(uGx=x\wedge xGu=x\right)\wedge \forall x\in X\left(yGx=x\wedge xGy=x\right)\right)\to u=y\right)$$
21	20	rgen2	$$⊢\forall u\in X\forall y\in X\left(\left(\forall x\in X\left(uGx=x\wedge xGu=x\right)\wedge \forall x\in X\left(yGx=x\wedge xGy=x\right)\right)\to u=y\right)$$
22		oveq1	$$⊢u=y\to uGx=yGx$$
23	22	eqeq1d	$$⊢u=y\to \left(uGx=x\leftrightarrow yGx=x\right)$$
24	23	ovanraleqv	$$⊢u=y\to \left(\forall x\in X\left(uGx=x\wedge xGu=x\right)\leftrightarrow \forall x\in X\left(yGx=x\wedge xGy=x\right)\right)$$
25	24	reu4	$$⊢\exists !u\in X\forall x\in X\left(uGx=x\wedge xGu=x\right)\leftrightarrow \left(\exists u\in X\forall x\in X\left(uGx=x\wedge xGu=x\right)\wedge \forall u\in X\forall y\in X\left(\left(\forall x\in X\left(uGx=x\wedge xGu=x\right)\wedge \forall x\in X\left(yGx=x\wedge xGy=x\right)\right)\to u=y\right)\right)$$
26	2 21 25	sylanblrc	$$⊢G\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to \exists !u\in X\forall x\in X\left(uGx=x\wedge xGu=x\right)$$