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 = ( 𝑤 ∈ Grp ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤 ↾_s 𝑠 ) ∈ Grp } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubg	⊢ SubGrp
1		vw	⊢ 𝑤
2		cgrp	⊢ Grp
3		vs	⊢ 𝑠
4		cbs	⊢ Base
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( Base ‘ 𝑤 )
7	6	cpw	⊢ 𝒫 ( Base ‘ 𝑤 )
8		cress	⊢ ↾_s
9	3	cv	⊢ 𝑠
10	5 9 8	co	⊢ ( 𝑤 ↾_s 𝑠 )
11	10 2	wcel	⊢ ( 𝑤 ↾_s 𝑠 ) ∈ Grp
12	11 3 7	crab	⊢ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤 ↾_s 𝑠 ) ∈ Grp }
13	1 2 12	cmpt	⊢ ( 𝑤 ∈ Grp ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤 ↾_s 𝑠 ) ∈ Grp } )
14	0 13	wceq	⊢ SubGrp = ( 𝑤 ∈ Grp ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤 ↾_s 𝑠 ) ∈ Grp } )

Metamath Proof Explorer

Definition df-subg

Detailed syntax breakdown