Metamath Proof Explorer

Theorem smgrpassOLD

Description: Obsolete version of sgrpass as of 3-Feb-2020. A semigroup is associative. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis smgrpassOLD.1 ⊢ X = dom ⁡ dom ⁡ G
Assertion smgrpassOLD ⊢ G ∈ SemiGrp → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z

Proof

Step Hyp Ref Expression
1 smgrpassOLD.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 simpr ⊢ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z
4 2 3 biimtrdi ⊢ G ∈ SemiGrp → G ∈ SemiGrp → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z
5 4 pm2.43i ⊢ G ∈ SemiGrp → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z