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∈XxGy=y∧yGx=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∈XxGy=y∧yGx=y
6 5 anbi2d ⊢G∈A→G∈SemiGrp∧G∈ExId↔G∈SemiGrp∧∃x∈X∀y∈XxGy=y∧yGx=y
7 4 6 bitrid ⊢G∈A→G∈SemiGrp∩ExId↔G∈SemiGrp∧∃x∈X∀y∈XxGy=y∧yGx=y
8 3 7 bitrid ⊢G∈A→G∈MndOp↔G∈SemiGrp∧∃x∈X∀y∈XxGy=y∧yGx=y