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

Metamath Proof Explorer

Definition df-subg

Description: Define a subgroup of a group as a set of elements that is a group in its own right. Equivalently ( issubg2 ), a subgroup is a subset of the group that is closed for the group internal operation (see subgcl ), contains the neutral element of the group (see subg0 ) and contains the inverses for all of its elements (see subginvcl ). (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion df-subg 
|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Grp } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubg 
 |-  SubGrp
1 vw 
 |-  w
2 cgrp 
 |-  Grp
3 vs 
 |-  s
4 cbs 
 |-  Base
5 1 cv 
 |-  w
6 5 4 cfv 
 |-  ( Base ` w )
7 6 cpw 
 |-  ~P ( Base ` w )
8 cress 
 |-  |`s
9 3 cv 
 |-  s
10 5 9 8 co 
 |-  ( w |`s s )
11 10 2 wcel 
 |-  ( w |`s s ) e. Grp
12 11 3 7 crab 
 |-  { s e. ~P ( Base ` w ) | ( w |`s s ) e. Grp }
13 1 2 12 cmpt 
 |-  ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Grp } )
14 0 13 wceq 
 |-  SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Grp } )