Metamath Proof Explorer

Theorem exidu1

Description: 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.)

Ref Expression
Hypothesis exidu1.1 ⊢X=ran⁡G
Assertion exidu1 ⊢G∈Magma∩ExId→∃!u∈X∀x∈XuGx=x∧xGu=x

Proof

Step Hyp Ref Expression
1 exidu1.1 ⊢X=ran⁡G
2 1 isexid2 ⊢G∈Magma∩ExId→∃u∈X∀x∈XuGx=x∧xGu=x
3 simpl ⊢uGx=x∧xGu=x→uGx=x
4 3 ralimi ⊢∀x∈XuGx=x∧xGu=x→∀x∈XuGx=x
5 oveq2 ⊢x=y→uGx=uGy
6 id ⊢x=y→x=y
7 5 6 eqeq12d ⊢x=y→uGx=x↔uGy=y
8 7 rspcv ⊢y∈X→∀x∈XuGx=x→uGy=y
9 4 8 syl5 ⊢y∈X→∀x∈XuGx=x∧xGu=x→uGy=y
10 simpr ⊢yGx=x∧xGy=x→xGy=x
11 10 ralimi ⊢∀x∈XyGx=x∧xGy=x→∀x∈XxGy=x
12 oveq1 ⊢x=u→xGy=uGy
13 id ⊢x=u→x=u
14 12 13 eqeq12d ⊢x=u→xGy=x↔uGy=u
15 14 rspcv ⊢u∈X→∀x∈XxGy=x→uGy=u
16 11 15 syl5 ⊢u∈X→∀x∈XyGx=x∧xGy=x→uGy=u
17 9 16 im2anan9r ⊢u∈X∧y∈X→∀x∈XuGx=x∧xGu=x∧∀x∈XyGx=x∧xGy=x→uGy=y∧uGy=u
18 eqtr2 ⊢uGy=y∧uGy=u→y=u
19 18 equcomd ⊢uGy=y∧uGy=u→u=y
20 17 19 syl6 ⊢u∈X∧y∈X→∀x∈XuGx=x∧xGu=x∧∀x∈XyGx=x∧xGy=x→u=y
21 20 rgen2 ⊢∀u∈X∀y∈X∀x∈XuGx=x∧xGu=x∧∀x∈XyGx=x∧xGy=x→u=y
22 oveq1 ⊢u=y→uGx=yGx
23 22 eqeq1d ⊢u=y→uGx=x↔yGx=x
24 23 ovanraleqv ⊢u=y→∀x∈XuGx=x∧xGu=x↔∀x∈XyGx=x∧xGy=x
25 24 reu4 ⊢∃!u∈X∀x∈XuGx=x∧xGu=x↔∃u∈X∀x∈XuGx=x∧xGu=x∧∀u∈X∀y∈X∀x∈XuGx=x∧xGu=x∧∀x∈XyGx=x∧xGy=x→u=y
26 2 21 25 sylanblrc ⊢G∈Magma∩ExId→∃!u∈X∀x∈XuGx=x∧xGu=x