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 e. ( Magma i^i ExId ) -> E! u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) )

Proof

Step Hyp Ref Expression
1 exidu1.1
 |-  X = ran G
2 1 isexid2
 |-  ( G e. ( Magma i^i ExId ) -> E. u e. X A. x e. 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
 |-  ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> A. x e. 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 e. X -> ( A. x e. X ( u G x ) = x -> ( u G y ) = y ) )
9 4 8 syl5
 |-  ( y e. X -> ( A. x e. 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
 |-  ( A. x e. X ( ( y G x ) = x /\ ( x G y ) = x ) -> A. x e. 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 e. X -> ( A. x e. X ( x G y ) = x -> ( u G y ) = u ) )
16 11 15 syl5
 |-  ( u e. X -> ( A. x e. X ( ( y G x ) = x /\ ( x G y ) = x ) -> ( u G y ) = u ) )
17 9 16 im2anan9r
 |-  ( ( u e. X /\ y e. X ) -> ( ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) /\ A. x e. 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 e. X /\ y e. X ) -> ( ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) /\ A. x e. X ( ( y G x ) = x /\ ( x G y ) = x ) ) -> u = y ) )
21 20 rgen2
 |-  A. u e. X A. y e. X ( ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) /\ A. x e. 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 -> ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) <-> A. x e. X ( ( y G x ) = x /\ ( x G y ) = x ) ) )
25 24 reu4
 |-  ( E! u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) <-> ( E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) /\ A. u e. X A. y e. X ( ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) /\ A. x e. X ( ( y G x ) = x /\ ( x G y ) = x ) ) -> u = y ) ) )
26 2 21 25 sylanblrc
 |-  ( G e. ( Magma i^i ExId ) -> E! u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) )