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 \in SemiGrp \to G : X \times X ⟶ X$

Step	Hyp	Ref	Expression
1		smgrpmgm.1	$⊢ X = dom dom G$
2	1	issmgrpOLD	$⊢ G \in SemiGrp \to (G \in SemiGrp \leftrightarrow (G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z)))$
3		simpl	$⊢ (G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z)) \to G : X \times X ⟶ X$
4	2 3	biimtrdi	$⊢ G \in SemiGrp \to (G \in SemiGrp \to G : X \times X ⟶ X)$
5	4	pm2.43i	$⊢ G \in SemiGrp \to G : X \times X ⟶ X$

Metamath Proof Explorer