Metamath Proof Explorer

Theorem ismndo

Description: The predicate "is a monoid". (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis ismndo.1 ⊢ X = dom ⁡ dom ⁡ G
Assertion ismndo ⊢ G ∈ A → G ∈ MndOp ↔ G ∈ SemiGrp ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y

Proof

Step Hyp Ref Expression
1 ismndo.1 ⊢ X = dom ⁡ dom ⁡ G
2 df-mndo ⊢ MndOp = SemiGrp ∩ ExId
3 2 eleq2i ⊢ G ∈ MndOp ↔ G ∈ SemiGrp ∩ ExId
4 elin ⊢ G ∈ SemiGrp ∩ ExId ↔ G ∈ SemiGrp ∧ G ∈ ExId
5 1 isexid ⊢ G ∈ A → G ∈ ExId ↔ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y
6 5 anbi2d ⊢ G ∈ A → G ∈ SemiGrp ∧ G ∈ ExId ↔ G ∈ SemiGrp ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y
7 4 6 syl5bb ⊢ G ∈ A → G ∈ SemiGrp ∩ ExId ↔ G ∈ SemiGrp ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y
8 3 7 syl5bb ⊢ G ∈ A → G ∈ MndOp ↔ G ∈ SemiGrp ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y