This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-submnd

Description: A submonoid is a subset of a monoid which contains the identity and is closed under the operation. Such subsets are themselves monoids with the same identity. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Assertion df-submnd ⊢ SubMnd = s ∈ Mnd ⟼ t ∈ 𝒫 Base s | 0 s ∈ t ∧ ∀ x ∈ t ∀ y ∈ t x + s y ∈ t

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubmnd class SubMnd
1 vs setvar s
2 cmnd class Mnd
3 vt setvar t
4 cbs class Base
5 1 cv setvar s
6 5 4 cfv class Base s
7 6 cpw class 𝒫 Base s
8 c0g class 0 𝑔
9 5 8 cfv class 0 s
10 3 cv setvar t
11 9 10 wcel wff 0 s ∈ t
12 vx setvar x
13 vy setvar y
14 12 cv setvar x
15 cplusg class + 𝑔
16 5 15 cfv class + s
17 13 cv setvar y
18 14 17 16 co class x + s y
19 18 10 wcel wff x + s y ∈ t
20 19 13 10 wral wff ∀ y ∈ t x + s y ∈ t
21 20 12 10 wral wff ∀ x ∈ t ∀ y ∈ t x + s y ∈ t
22 11 21 wa wff 0 s ∈ t ∧ ∀ x ∈ t ∀ y ∈ t x + s y ∈ t
23 22 3 7 crab class t ∈ 𝒫 Base s | 0 s ∈ t ∧ ∀ x ∈ t ∀ y ∈ t x + s y ∈ t
24 1 2 23 cmpt class s ∈ Mnd ⟼ t ∈ 𝒫 Base s | 0 s ∈ t ∧ ∀ x ∈ t ∀ y ∈ t x + s y ∈ t
25 0 24 wceq wff SubMnd = s ∈ Mnd ⟼ t ∈ 𝒫 Base s | 0 s ∈ t ∧ ∀ x ∈ t ∀ y ∈ t x + s y ∈ t