Theorem smgrpmgm

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

	Ref	Expression
Hypothesis	smgrpmgm.1	$$⊢X=\mathrm{dom}\mathrm{dom}G$$
Assertion	smgrpmgm	$$⊢G\in \mathrm{SemiGrp}\to G:X\times X⟶X$$

Proof

Step	Hyp	Ref	Expression
1		smgrpmgm.1	$$⊢X=\mathrm{dom}\mathrm{dom}G$$
2	1	issmgrpOLD	$$⊢G\in \mathrm{SemiGrp}\to \left(G\in \mathrm{SemiGrp}\leftrightarrow \left(G:X\times X⟶X\wedge \forall x\in X\forall y\in X\forall z\in X\left(xGy\right)Gz=xG\left(yGz\right)\right)\right)$$
3		simpl	$$⊢\left(G:X\times X⟶X\wedge \forall x\in X\forall y\in X\forall z\in X\left(xGy\right)Gz=xG\left(yGz\right)\right)\to G:X\times X⟶X$$
4	2 3	syl6bi	$$⊢G\in \mathrm{SemiGrp}\to \left(G\in \mathrm{SemiGrp}\to G:X\times X⟶X\right)$$
5	4	pm2.43i	$$⊢G\in \mathrm{SemiGrp}\to G:X\times X⟶X$$