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