Definition df-slw 17951

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

Assertion

Ref	Expression
df-slw	|- pSyl = ( p e. Prime , g e. Grp |-> { h e. (SubGrp ` g ) | A. k e. (SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g ↾s k ) ) <-> h = k ) } )

Distinct variable group:   g, h, k, p

Detailed syntax breakdown of Definition df-slw

Step	Hyp	Ref	Expression
1		cslw 17947	. 2 class pSyl
2		vp	. . 3 setvar p
3		vg	. . 3 setvar g
4		cprime 15385	. . 3 class Prime
5		cgrp 17422	. . 3 class Grp
6		vh	. . . . . . . . 9 setvar h
7	6	cv 1482	. . . . . . . 8 class h
8		vk	. . . . . . . . 9 setvar k
9	8	cv 1482	. . . . . . . 8 class k
10	7, 9	wss 3574	. . . . . . 7 wff h C_ k
11	2	cv 1482	. . . . . . . 8 class p
12	3	cv 1482	. . . . . . . . 9 class g
13		cress 15858	. . . . . . . . 9 class ↾s
14	12, 9, 13	co 6650	. . . . . . . 8 class ( g ↾s k )
15		cpgp 17946	. . . . . . . 8 class pGrp
16	11, 14, 15	wbr 4653	. . . . . . 7 wff p pGrp ( g ↾s k )
17	10, 16	wa 384	. . . . . 6 wff ( h C_ k /\ p pGrp ( g ↾s k ) )
18	6, 8	weq 1874	. . . . . 6 wff h = k
19	17, 18	wb 196	. . . . 5 wff ( ( h C_ k /\ p pGrp ( g ↾s k ) ) <-> h = k )
20		csubg 17588	. . . . . 6 class SubGrp
21	12, 20	cfv 5888	. . . . 5 class (SubGrp ` g )
22	19, 8, 21	wral 2912	. . . 4 wff A. k e. (SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g ↾s k ) ) <-> h = k )
23	22, 6, 21	crab 2916	. . 3 class { h e. (SubGrp ` g ) | A. k e. (SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g ↾s k ) ) <-> h = k ) }
24	2, 3, 4, 5, 23	cmpt2 6652	. 2 class ( p e. Prime , g e. Grp |-> { h e. (SubGrp ` g ) | A. k e. (SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g ↾s k ) ) <-> h = k ) } )
25	1, 24	wceq 1483	1 wff pSyl = ( p e. Prime , g e. Grp |-> { h e. (SubGrp ` g ) | A. k e. (SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g ↾s k ) ) <-> h = k ) } )

This definition is referenced by:  isslw  18023