Metamath Proof Explorer

Theorem issmgrpOLD

Description: Obsolete version of issgrp as of 3-Feb-2020. The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis issmgrpOLD.1 ⊢ X = dom ⁡ dom ⁡ G
Assertion issmgrpOLD ⊢ G ∈ A → G ∈ SemiGrp ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z

Proof

Step Hyp Ref Expression
1 issmgrpOLD.1 ⊢ X = dom ⁡ dom ⁡ G
2 df-sgrOLD ⊢ SemiGrp = Magma ∩ Ass
3 2 eleq2i ⊢ G ∈ SemiGrp ↔ G ∈ Magma ∩ Ass
4 elin ⊢ G ∈ Magma ∩ Ass ↔ G ∈ Magma ∧ G ∈ Ass
5 1 ismgmOLD ⊢ G ∈ A → G ∈ Magma ↔ G : X × X ⟶ X
6 1 isass ⊢ G ∈ A → G ∈ Ass ↔ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z
7 5 6 anbi12d ⊢ G ∈ A → G ∈ Magma ∧ G ∈ Ass ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z
8 4 7 syl5bb ⊢ G ∈ A → G ∈ Magma ∩ Ass ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z
9 3 8 syl5bb ⊢ G ∈ A → G ∈ SemiGrp ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z