This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑝 ∈ ℙ , 𝑔 ∈ 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 𝑘 ) ) ↔ ℎ = 𝑘 ) } )