Description: Obsolete version of mndsgrp as of 3-Feb-2020. A monoid is a semigroup. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | mndoissmgrpOLD | ⊢ ( 𝐺 ∈ MndOp → 𝐺 ∈ SemiGrp ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elin | ⊢ ( 𝐺 ∈ ( SemiGrp ∩ ExId ) ↔ ( 𝐺 ∈ SemiGrp ∧ 𝐺 ∈ ExId ) ) | |
| 2 | 1 | simplbi | ⊢ ( 𝐺 ∈ ( SemiGrp ∩ ExId ) → 𝐺 ∈ SemiGrp ) |
| 3 | df-mndo | ⊢ MndOp = ( SemiGrp ∩ ExId ) | |
| 4 | 2 3 | eleq2s | ⊢ ( 𝐺 ∈ MndOp → 𝐺 ∈ SemiGrp ) |