# 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 𝑋 = ran 𝐺
Assertion exidu1 ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃! 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )

### Proof

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