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 ∈ Grp ⟼ s ∈ 𝒫 Base w | w ↾ 𝑠 s ∈ Grp

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubg class SubGrp
1 vw setvar w
2 cgrp class Grp
3 vs setvar s
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 6 cpw class 𝒫 Base w
8 cress class ↾ 𝑠
9 3 cv setvar s
10 5 9 8 co class w ↾ 𝑠 s
11 10 2 wcel wff w ↾ 𝑠 s ∈ Grp
12 11 3 7 crab class s ∈ 𝒫 Base w | w ↾ 𝑠 s ∈ Grp
13 1 2 12 cmpt class w ∈ Grp ⟼ s ∈ 𝒫 Base w | w ↾ 𝑠 s ∈ Grp
14 0 13 wceq wff SubGrp = w ∈ Grp ⟼ s ∈ 𝒫 Base w | w ↾ 𝑠 s ∈ Grp