Definition df-subg 13673

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

Assertion

Ref	Expression
df-subg	⊢ SubGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp})

Distinct variable group:   𝑤,𝑠

Detailed syntax breakdown of Definition df-subg

Step	Hyp	Ref	Expression
1		csubg 13670	. 2 class SubGrp
2		vw	. . 3 setvar 𝑤
3		cgrp 13499	. . 3 class Grp
4	2	cv 1374	. . . . . 6 class 𝑤
5		vs	. . . . . . 7 setvar 𝑠
6	5	cv 1374	. . . . . 6 class 𝑠
7		cress 12999	. . . . . 6 class ↾s
8	4, 6, 7	co 5974	. . . . 5 class (𝑤 ↾s 𝑠)
9	8, 3	wcel 2180	. . . 4 wff (𝑤 ↾s 𝑠) ∈ Grp
10		cbs 12998	. . . . . 6 class Base
11	4, 10	cfv 5294	. . . . 5 class (Base‘𝑤)
12	11	cpw 3629	. . . 4 class 𝒫 (Base‘𝑤)
13	9, 5, 12	crab 2492	. . 3 class {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp}
14	2, 3, 13	cmpt 4124	. 2 class (𝑤 ∈ Grp ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp})
15	1, 14	wceq 1375	1 wff SubGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp})

This definition is referenced by:  issubg  13676  subgex  13679