Metamath Proof Explorer

Theorem submgmid

Description: Every magma is trivially a submagma of itself. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypothesis submgmss.b ⊢ B = Base M
Assertion submgmid ⊢ M ∈ Mgm → B ∈ SubMgm ⁡ M

Proof

Step Hyp Ref Expression
1 submgmss.b ⊢ B = Base M
2 ssidd ⊢ M ∈ Mgm → B ⊆ B
3 1 ressid ⊢ M ∈ Mgm → M ↾ 𝑠 B = M
4 id ⊢ M ∈ Mgm → M ∈ Mgm
5 3 4 eqeltrd ⊢ M ∈ Mgm → M ↾ 𝑠 B ∈ Mgm
6 eqid ⊢ M ↾ 𝑠 B = M ↾ 𝑠 B
7 1 6 issubmgm2 ⊢ M ∈ Mgm → B ∈ SubMgm ⁡ M ↔ B ⊆ B ∧ M ↾ 𝑠 B ∈ Mgm
8 2 5 7 mpbir2and ⊢ M ∈ Mgm → B ∈ SubMgm ⁡ M