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 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 ) } )