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

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 
|- SubMgm = ( s e. Mgm |-> { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubmgm 
 |-  SubMgm
1 vs 
 |-  s
2 cmgm 
 |-  Mgm
3 vt 
 |-  t
4 cbs 
 |-  Base
5 1 cv 
 |-  s
6 5 4 cfv 
 |-  ( Base ` s )
7 6 cpw 
 |-  ~P ( Base ` s )
8 vx 
 |-  x
9 3 cv 
 |-  t
10 vy 
 |-  y
11 8 cv 
 |-  x
12 cplusg 
 |-  +g
13 5 12 cfv 
 |-  ( +g ` s )
14 10 cv 
 |-  y
15 11 14 13 co 
 |-  ( x ( +g ` s ) y )
16 15 9 wcel 
 |-  ( x ( +g ` s ) y ) e. t
17 16 10 9 wral 
 |-  A. y e. t ( x ( +g ` s ) y ) e. t
18 17 8 9 wral 
 |-  A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t
19 18 3 7 crab 
 |-  { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t }
20 1 2 19 cmpt 
 |-  ( s e. Mgm |-> { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t } )
21 0 20 wceq 
 |-  SubMgm = ( s e. Mgm |-> { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t } )