Definition df-slw

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cslw	⊢ pSyl
1		vp	⊢ 𝑝
2		cprime	⊢ ℙ
3		vg	⊢ 𝑔
4		cgrp	⊢ Grp
5		vh	⊢ ℎ
6		csubg	⊢ SubGrp
7	3	cv	⊢ 𝑔
8	7 6	cfv	⊢ ( SubGrp ‘ 𝑔 )
9		vk	⊢ 𝑘
10	5	cv	⊢ ℎ
11	9	cv	⊢ 𝑘
12	10 11	wss	⊢ ℎ ⊆ 𝑘
13	1	cv	⊢ 𝑝
14		cpgp	⊢ pGrp
15		cress	⊢ ↾s
16	7 11 15	co	⊢ ( 𝑔 ↾s 𝑘 )
17	13 16 14	wbr	⊢ 𝑝 pGrp ( 𝑔 ↾s 𝑘 )
18	12 17	wa	⊢ ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) )
19	10 11	wceq	⊢ ℎ = 𝑘
20	18 19	wb	⊢ ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 )
21	20 9 8	wral	⊢ ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 )
22	21 5 8	crab	⊢ { ℎ ∈ ( SubGrp ‘ 𝑔 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) }
23	1 3 2 4 22	cmpo	⊢ ( 𝑝 ∈ ℙ , 𝑔 ∈ Grp ↦ { ℎ ∈ ( SubGrp ‘ 𝑔 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) } )
24	0 23	wceq	⊢ pSyl = ( 𝑝 ∈ ℙ , 𝑔 ∈ Grp ↦ { ℎ ∈ ( SubGrp ‘ 𝑔 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) } )