Metamath Proof Explorer


Theorem isexid2

Description: If G e. ( Magma i^i ExId ) , then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis isexid2.1
|- X = ran G
Assertion isexid2
|- ( 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 isexid2.1
 |-  X = ran G
2 rngopidOLD
 |-  ( G e. ( Magma i^i ExId ) -> ran G = dom dom G )
3 elin
 |-  ( G e. ( Magma i^i ExId ) <-> ( G e. Magma /\ G e. ExId ) )
4 eqid
 |-  dom dom G = dom dom G
5 4 isexid
 |-  ( G e. ExId -> ( G e. ExId <-> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) )
6 5 ibi
 |-  ( G e. ExId -> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) )
7 6 a1d
 |-  ( G e. ExId -> ( X = dom dom G -> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) )
8 7 adantl
 |-  ( ( G e. Magma /\ G e. ExId ) -> ( X = dom dom G -> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) )
9 3 8 sylbi
 |-  ( G e. ( Magma i^i ExId ) -> ( X = dom dom G -> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) )
10 eqeq2
 |-  ( ran G = dom dom G -> ( X = ran G <-> X = dom dom G ) )
11 raleq
 |-  ( ran G = dom dom G -> ( A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) <-> A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) )
12 11 rexeqbi1dv
 |-  ( ran G = dom dom G -> ( E. u e. ran G A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) <-> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) )
13 10 12 imbi12d
 |-  ( ran G = dom dom G -> ( ( X = ran G -> E. u e. ran G A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) ) <-> ( X = dom dom G -> E. u e. dom dom G A. x e. dom dom G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) )
14 9 13 syl5ibr
 |-  ( ran G = dom dom G -> ( G e. ( Magma i^i ExId ) -> ( X = ran G -> E. u e. ran G A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) ) ) )
15 2 14 mpcom
 |-  ( G e. ( Magma i^i ExId ) -> ( X = ran G -> E. u e. ran G A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) ) )
16 15 com12
 |-  ( X = ran G -> ( G e. ( Magma i^i ExId ) -> E. u e. ran G A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) ) )
17 raleq
 |-  ( X = ran G -> ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) <-> A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) ) )
18 17 rexeqbi1dv
 |-  ( X = ran G -> ( E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) <-> E. u e. ran G A. x e. ran G ( ( u G x ) = x /\ ( x G u ) = x ) ) )
19 16 18 sylibrd
 |-  ( X = ran G -> ( G e. ( Magma i^i ExId ) -> E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
20 1 19 ax-mp
 |-  ( G e. ( Magma i^i ExId ) -> E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) )