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 ∈ X u G x = x ∧ x G u = x

Proof

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