This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )