Theorem smgrpmgm

Description: A semigroup is a magma. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.)

	Ref	Expression
Hypothesis	smgrpmgm.1	|- X = dom dom G
Assertion	smgrpmgm	|- ( G e. SemiGrp -> G : ( X X. X ) --> X )

Proof

Step	Hyp	Ref	Expression
1		smgrpmgm.1	|- X = dom dom G
2	1	issmgrpOLD	|- ( G e. SemiGrp -> ( 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 ) ) ) ) )
3		simpl	|- ( ( 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 ) ) ) -> G : ( X X. X ) --> X )
4	2 3	syl6bi	|- ( G e. SemiGrp -> ( G e. SemiGrp -> G : ( X X. X ) --> X ) )
5	4	pm2.43i	|- ( G e. SemiGrp -> G : ( X X. X ) --> X )