Metamath Proof Explorer

Theorem isslw

Description: The property of being a Sylow subgroup. A Sylow P -subgroup is a P -group which has no proper supersets that are also P -groups. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Assertion isslw ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 df-slw ⊢ pSyl = ( 𝑝 ∈ ℙ , 𝑔 ∈ Grp ↦ { ℎ ∈ ( SubGrp ‘ 𝑔 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) } )
2 1 elmpocl ⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) )
3 simp1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) → 𝑃 ∈ ℙ )
4 subgrcl ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
5 4 3ad2ant2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) → 𝐺 ∈ Grp )
6 3 5 jca ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) → ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) )
7 simpr ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
8 7 fveq2d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( SubGrp ‘ 𝑔 ) = ( SubGrp ‘ 𝐺 ) )
9 simpl ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → 𝑝 = 𝑃 )
10 7 oveq1d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( 𝑔 ↾s 𝑘 ) = ( 𝐺 ↾s 𝑘 ) )
11 9 10 breq12d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ↔ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) )
12 11 anbi2d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ( ℎ ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) )
13 12 bibi1d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) ↔ ( ( ℎ ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) ) )
14 8 13 raleqbidv ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) ↔ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) ) )
15 8 14 rabeqbidv ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → { ℎ ∈ ( SubGrp ‘ 𝑔 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) } = { ℎ ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) } )
16 fvex ⊢ ( SubGrp ‘ 𝐺 ) ∈ V
17 16 rabex ⊢ { ℎ ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) } ∈ V
18 15 1 17 ovmpoa ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → ( 𝑃 pSyl 𝐺 ) = { ℎ ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) } )
19 18 eleq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ 𝐻 ∈ { ℎ ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) } ) )
20 cleq1lem ⊢ ( ℎ = 𝐻 → ( ( ℎ ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) )
21 eqeq1 ⊢ ( ℎ = 𝐻 → ( ℎ = 𝑘 ↔ 𝐻 = 𝑘 ) )
22 20 21 bibi12d ⊢ ( ℎ = 𝐻 → ( ( ( ℎ ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) ↔ ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) )
23 22 ralbidv ⊢ ( ℎ = 𝐻 → ( ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) ↔ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) )
24 23 elrab ⊢ ( 𝐻 ∈ { ℎ ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) } ↔ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) )
25 19 24 bitrdi ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ) )
26 simpl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → 𝑃 ∈ ℙ )
27 26 biantrurd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ↔ ( 𝑃 ∈ ℙ ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ) ) )
28 25 27 bitrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝑃 ∈ ℙ ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ) ) )
29 3anass ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ↔ ( 𝑃 ∈ ℙ ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ) )
30 28 29 bitr4di ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ) )
31 2 6 30 pm5.21nii ⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) )