Theorem isabloi

Description: Properties that determine an Abelian group operation. (Contributed by NM, 5-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isabli.1	|- G e. GrpOp
	isabli.2	|- dom G = ( X X. X )
	isabli.3	|- ( ( x e. X /\ y e. X ) -> ( x G y ) = ( y G x ) )
Assertion	isabloi	|- G e. AbelOp

Proof

Step	Hyp	Ref	Expression
1		isabli.1	|- G e. GrpOp
2		isabli.2	|- dom G = ( X X. X )
3		isabli.3	|- ( ( x e. X /\ y e. X ) -> ( x G y ) = ( y G x ) )
4	3	rgen2	|- A. x e. X A. y e. X ( x G y ) = ( y G x )
5	1 2	grporn	|- X = ran G
6	5	isablo	|- ( G e. AbelOp <-> ( G e. GrpOp /\ A. x e. X A. y e. X ( x G y ) = ( y G x ) ) )
7	1 4 6	mpbir2an	|- G e. AbelOp