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