Definition df-slw 19054

Description: Define the set of Sylow p-subgroups of a group 𝑔. A Sylow p-subgroup is a p-group that is not a subgroup of any other p-groups in 𝑔. (Contributed by Mario Carneiro, 16-Jan-2015.)

Assertion

Ref	Expression
df-slw	⊢ pSyl = (𝑝 ∈ ℙ, 𝑔 ∈ Grp ↦ {ℎ ∈ (SubGrp‘𝑔) ∣ ∀𝑘 ∈ (SubGrp‘𝑔)((ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘)) ↔ ℎ = 𝑘)})

Distinct variable group:   𝑔,ℎ,𝑘,𝑝

Detailed syntax breakdown of Definition df-slw

Step	Hyp	Ref	Expression
1		cslw 19050	. 2 class pSyl
2		vp	. . 3 setvar 𝑝
3		vg	. . 3 setvar 𝑔
4		cprime 16304	. . 3 class ℙ
5		cgrp 18492	. . 3 class Grp
6		vh	. . . . . . . . 9 setvar ℎ
7	6	cv 1538	. . . . . . . 8 class ℎ
8		vk	. . . . . . . . 9 setvar 𝑘
9	8	cv 1538	. . . . . . . 8 class 𝑘
10	7, 9	wss 3883	. . . . . . 7 wff ℎ ⊆ 𝑘
11	2	cv 1538	. . . . . . . 8 class 𝑝
12	3	cv 1538	. . . . . . . . 9 class 𝑔
13		cress 16867	. . . . . . . . 9 class ↾s
14	12, 9, 13	co 7255	. . . . . . . 8 class (𝑔 ↾s 𝑘)
15		cpgp 19049	. . . . . . . 8 class pGrp
16	11, 14, 15	wbr 5070	. . . . . . 7 wff 𝑝 pGrp (𝑔 ↾s 𝑘)
17	10, 16	wa 395	. . . . . 6 wff (ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘))
18	6, 8	weq 1967	. . . . . 6 wff ℎ = 𝑘
19	17, 18	wb 205	. . . . 5 wff ((ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘)) ↔ ℎ = 𝑘)
20		csubg 18664	. . . . . 6 class SubGrp
21	12, 20	cfv 6418	. . . . 5 class (SubGrp‘𝑔)
22	19, 8, 21	wral 3063	. . . 4 wff ∀𝑘 ∈ (SubGrp‘𝑔)((ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘)) ↔ ℎ = 𝑘)
23	22, 6, 21	crab 3067	. . 3 class {ℎ ∈ (SubGrp‘𝑔) ∣ ∀𝑘 ∈ (SubGrp‘𝑔)((ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘)) ↔ ℎ = 𝑘)}
24	2, 3, 4, 5, 23	cmpo 7257	. 2 class (𝑝 ∈ ℙ, 𝑔 ∈ Grp ↦ {ℎ ∈ (SubGrp‘𝑔) ∣ ∀𝑘 ∈ (SubGrp‘𝑔)((ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘)) ↔ ℎ = 𝑘)})
25	1, 24	wceq 1539	1 wff pSyl = (𝑝 ∈ ℙ, 𝑔 ∈ Grp ↦ {ℎ ∈ (SubGrp‘𝑔) ∣ ∀𝑘 ∈ (SubGrp‘𝑔)((ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘)) ↔ ℎ = 𝑘)})

This definition is referenced by:  isslw  19128