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

Metamath Proof Explorer

Theorem isexid

Description: The predicate G has a left and right identity element. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis isexid.1 
|- X = dom dom G
Assertion isexid 
|- ( G e. A -> ( G e. ExId <-> E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) )

Proof

Step Hyp Ref Expression
1 isexid.1 
 |-  X = dom dom G
2 dmeq 
 |-  ( g = G -> dom g = dom G )
3 2 dmeqd 
 |-  ( g = G -> dom dom g = dom dom G )
4 3 1 eqtr4di 
 |-  ( g = G -> dom dom g = X )
5 oveq 
 |-  ( g = G -> ( x g y ) = ( x G y ) )
6 5 eqeq1d 
 |-  ( g = G -> ( ( x g y ) = y <-> ( x G y ) = y ) )
7 oveq 
 |-  ( g = G -> ( y g x ) = ( y G x ) )
8 7 eqeq1d 
 |-  ( g = G -> ( ( y g x ) = y <-> ( y G x ) = y ) )
9 6 8 anbi12d 
 |-  ( g = G -> ( ( ( x g y ) = y /\ ( y g x ) = y ) <-> ( ( x G y ) = y /\ ( y G x ) = y ) ) )
10 4 9 raleqbidv 
 |-  ( g = G -> ( A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y ) <-> A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) )
11 4 10 rexeqbidv 
 |-  ( g = G -> ( E. x e. dom dom g A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y ) <-> E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) )
12 df-exid 
 |-  ExId = { g | E. x e. dom dom g A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y ) }
13 11 12 elab2g 
 |-  ( G e. A -> ( G e. ExId <-> E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) )