# Metamath Proof Explorer

## Definition df-submgm

Description: A submagma is a subset of a magma which is closed under the operation. Such subsets are themselves magmas. (Contributed by AV, 24-Feb-2020)

Ref Expression
Assertion df-submgm ${⊢}\mathrm{SubMgm}=\left({s}\in \mathrm{Mgm}⟼\left\{{t}\in 𝒫{\mathrm{Base}}_{{s}}|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{s}}{y}\in {t}\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 csubmgm ${class}\mathrm{SubMgm}$
1 vs ${setvar}{s}$
2 cmgm ${class}\mathrm{Mgm}$
3 vt ${setvar}{t}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{s}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{s}}$
7 6 cpw ${class}𝒫{\mathrm{Base}}_{{s}}$
8 vx ${setvar}{x}$
9 3 cv ${setvar}{t}$
10 vy ${setvar}{y}$
11 8 cv ${setvar}{x}$
12 cplusg ${class}{+}_{𝑔}$
13 5 12 cfv ${class}{+}_{{s}}$
14 10 cv ${setvar}{y}$
15 11 14 13 co ${class}\left({x}{+}_{{s}}{y}\right)$
16 15 9 wcel ${wff}{x}{+}_{{s}}{y}\in {t}$
17 16 10 9 wral ${wff}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{s}}{y}\in {t}$
18 17 8 9 wral ${wff}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{s}}{y}\in {t}$
19 18 3 7 crab ${class}\left\{{t}\in 𝒫{\mathrm{Base}}_{{s}}|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{s}}{y}\in {t}\right\}$
20 1 2 19 cmpt ${class}\left({s}\in \mathrm{Mgm}⟼\left\{{t}\in 𝒫{\mathrm{Base}}_{{s}}|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{s}}{y}\in {t}\right\}\right)$
21 0 20 wceq ${wff}\mathrm{SubMgm}=\left({s}\in \mathrm{Mgm}⟼\left\{{t}\in 𝒫{\mathrm{Base}}_{{s}}|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{s}}{y}\in {t}\right\}\right)$