Metamath Proof Explorer

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 = p ∈ ℙ , g ∈ Grp ⟼ h ∈ SubGrp ⁡ g | ∀ k ∈ SubGrp ⁡ g h ⊆ k ∧ p pGrp g ↾ 𝑠 k ↔ h = k

Detailed syntax breakdown

Step Hyp Ref Expression
0 cslw class pSyl
1 vp setvar p
2 cprime class ℙ
3 vg setvar g
4 cgrp class Grp
5 vh setvar h
6 csubg class SubGrp
7 3 cv setvar g
8 7 6 cfv class SubGrp ⁡ g
9 vk setvar k
10 5 cv setvar h
11 9 cv setvar k
12 10 11 wss wff h ⊆ k
13 1 cv setvar p
14 cpgp class pGrp
15 cress class ↾ 𝑠
16 7 11 15 co class g ↾ 𝑠 k
17 13 16 14 wbr wff p pGrp g ↾ 𝑠 k
18 12 17 wa wff h ⊆ k ∧ p pGrp g ↾ 𝑠 k
19 10 11 wceq wff h = k
20 18 19 wb wff h ⊆ k ∧ p pGrp g ↾ 𝑠 k ↔ h = k
21 20 9 8 wral wff ∀ k ∈ SubGrp ⁡ g h ⊆ k ∧ p pGrp g ↾ 𝑠 k ↔ h = k
22 21 5 8 crab class h ∈ SubGrp ⁡ g | ∀ k ∈ SubGrp ⁡ g h ⊆ k ∧ p pGrp g ↾ 𝑠 k ↔ h = k
23 1 3 2 4 22 cmpo class p ∈ ℙ , g ∈ Grp ⟼ h ∈ SubGrp ⁡ g | ∀ k ∈ SubGrp ⁡ g h ⊆ k ∧ p pGrp g ↾ 𝑠 k ↔ h = k
24 0 23 wceq wff pSyl = p ∈ ℙ , g ∈ Grp ⟼ h ∈ SubGrp ⁡ g | ∀ k ∈ SubGrp ⁡ g h ⊆ k ∧ p pGrp g ↾ 𝑠 k ↔ h = k