Metamath Proof Explorer

Theorem submid

Description: Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Hypothesis submss.b ⊢ B = Base M
Assertion submid ⊢ M ∈ Mnd → B ∈ SubMnd ⁡ M

Proof

Step Hyp Ref Expression
1 submss.b ⊢ B = Base M
2 ssidd ⊢ M ∈ Mnd → B ⊆ B
3 eqid ⊢ 0 M = 0 M
4 1 3 mndidcl ⊢ M ∈ Mnd → 0 M ∈ B
5 1 ressid ⊢ M ∈ Mnd → M ↾ 𝑠 B = M
6 id ⊢ M ∈ Mnd → M ∈ Mnd
7 5 6 eqeltrd ⊢ M ∈ Mnd → M ↾ 𝑠 B ∈ Mnd
8 eqid ⊢ M ↾ 𝑠 B = M ↾ 𝑠 B
9 1 3 8 issubm2 ⊢ M ∈ Mnd → B ∈ SubMnd ⁡ M ↔ B ⊆ B ∧ 0 M ∈ B ∧ M ↾ 𝑠 B ∈ Mnd
10 2 4 7 9 mpbir3and ⊢ M ∈ Mnd → B ∈ SubMnd ⁡ M