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	$$⊢\mathrm{SubGrp}=\left(w\in \mathrm{Grp}⟼\left\{s\in 𝒫{\mathrm{Base}}_w|w{\upharpoonright }_{𝑠}s\in \mathrm{Grp}\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubg	$$class\mathrm{SubGrp}$$
1		vw	$$setvarw$$
2		cgrp	$$class\mathrm{Grp}$$
3		vs	$$setvars$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class{\mathrm{Base}}_w$$
7	6	cpw	$$class𝒫{\mathrm{Base}}_w$$
8		cress	$$class{\upharpoonright }_{𝑠}$$
9	3	cv	$$setvars$$
10	5 9 8	co	$$class\left(w{\upharpoonright }_{𝑠}s\right)$$
11	10 2	wcel	$$wffw{\upharpoonright }_{𝑠}s\in \mathrm{Grp}$$
12	11 3 7	crab	$$class\left\{s\in 𝒫{\mathrm{Base}}_w|w{\upharpoonright }_{𝑠}s\in \mathrm{Grp}\right\}$$
13	1 2 12	cmpt	$$class\left(w\in \mathrm{Grp}⟼\left\{s\in 𝒫{\mathrm{Base}}_w|w{\upharpoonright }_{𝑠}s\in \mathrm{Grp}\right\}\right)$$
14	0 13	wceq	$$wff\mathrm{SubGrp}=\left(w\in \mathrm{Grp}⟼\left\{s\in 𝒫{\mathrm{Base}}_w|w{\upharpoonright }_{𝑠}s\in \mathrm{Grp}\right\}\right)$$