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