Metamath Proof Explorer

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 ∈ SemiGrp → G : X × X ⟶ X

Proof

Step Hyp Ref Expression
1 smgrpmgm.1 ⊢ X = dom ⁡ dom ⁡ G
2 1 issmgrpOLD ⊢ G ∈ SemiGrp → G ∈ SemiGrp ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z
3 simpl ⊢ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z → G : X × X ⟶ X
4 2 3 biimtrdi ⊢ G ∈ SemiGrp → G ∈ SemiGrp → G : X × X ⟶ X
5 4 pm2.43i ⊢ G ∈ SemiGrp → G : X × X ⟶ X