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 e. Mnd |-> { t e. ~P ( Base ` s ) | ( ( 0g ` s ) e. t /\ A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubmnd
 |-  SubMnd
1 vs
 |-  s
2 cmnd
 |-  Mnd
3 vt
 |-  t
4 cbs
 |-  Base
5 1 cv
 |-  s
6 5 4 cfv
 |-  ( Base ` s )
7 6 cpw
 |-  ~P ( Base ` s )
8 c0g
 |-  0g
9 5 8 cfv
 |-  ( 0g ` s )
10 3 cv
 |-  t
11 9 10 wcel
 |-  ( 0g ` s ) e. t
12 vx
 |-  x
13 vy
 |-  y
14 12 cv
 |-  x
15 cplusg
 |-  +g
16 5 15 cfv
 |-  ( +g ` s )
17 13 cv
 |-  y
18 14 17 16 co
 |-  ( x ( +g ` s ) y )
19 18 10 wcel
 |-  ( x ( +g ` s ) y ) e. t
20 19 13 10 wral
 |-  A. y e. t ( x ( +g ` s ) y ) e. t
21 20 12 10 wral
 |-  A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t
22 11 21 wa
 |-  ( ( 0g ` s ) e. t /\ A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t )
23 22 3 7 crab
 |-  { t e. ~P ( Base ` s ) | ( ( 0g ` s ) e. t /\ A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t ) }
24 1 2 23 cmpt
 |-  ( s e. Mnd |-> { t e. ~P ( Base ` s ) | ( ( 0g ` s ) e. t /\ A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t ) } )
25 0 24 wceq
 |-  SubMnd = ( s e. Mnd |-> { t e. ~P ( Base ` s ) | ( ( 0g ` s ) e. t /\ A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t ) } )