Theorem issmgrpOLD

Description: Obsolete version of issgrp as of 3-Feb-2020. The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	issmgrpOLD.1	|- X = dom dom G
Assertion	issmgrpOLD	|- ( G e. A -> ( G e. SemiGrp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		issmgrpOLD.1	|- X = dom dom G
2		df-sgrOLD	|- SemiGrp = ( Magma i^i Ass )
3	2	eleq2i	|- ( G e. SemiGrp <-> G e. ( Magma i^i Ass ) )
4		elin	|- ( G e. ( Magma i^i Ass ) <-> ( G e. Magma /\ G e. Ass ) )
5	1	ismgmOLD	|- ( G e. A -> ( G e. Magma <-> G : ( X X. X ) --> X ) )
6	1	isass	|- ( G e. A -> ( G e. Ass <-> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
7	5 6	anbi12d	|- ( G e. A -> ( ( G e. Magma /\ G e. Ass ) <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) ) )
8	4 7	syl5bb	|- ( G e. A -> ( G e. ( Magma i^i Ass ) <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) ) )
9	3 8	syl5bb	|- ( G e. A -> ( G e. SemiGrp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) ) )