Metamath Proof Explorer

Theorem fislw

Description: The sylow subgroups of a finite group are exactly the groups which have cardinality equal to the maximum power of P dividing the group. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis fislw.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion fislw ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fislw.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) )
3 slwsubg ⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
4 2 3 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
5 simpl2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝑋 ∈ Fin )
6 1 5 2 slwhash ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
7 4 6 jca ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
8 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝑃 ∈ ℙ )
9 simprl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
10 simpl2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝑋 ∈ Fin )
11 10 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝑋 ∈ Fin )
12 simprl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝑘 ∈ ( SubGrp ‘ 𝐺 ) )
13 1 subgss ⊢ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) → 𝑘 ⊆ 𝑋 )
14 12 13 syl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝑘 ⊆ 𝑋 )
15 11 14 ssfid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝑘 ∈ Fin )
16 simprrl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝐻 ⊆ 𝑘 )
17 ssdomg ⊢ ( 𝑘 ∈ Fin → ( 𝐻 ⊆ 𝑘 → 𝐻 ≼ 𝑘 ) )
18 15 16 17 sylc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝐻 ≼ 𝑘 )
19 simprrr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) )
20 eqid ⊢ ( 𝐺 ↾s 𝑘 ) = ( 𝐺 ↾s 𝑘 )
21 20 subggrp ⊢ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ↾s 𝑘 ) ∈ Grp )
22 12 21 syl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( 𝐺 ↾s 𝑘 ) ∈ Grp )
23 20 subgbas ⊢ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) → 𝑘 = ( Base ‘ ( 𝐺 ↾s 𝑘 ) ) )
24 12 23 syl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝑘 = ( Base ‘ ( 𝐺 ↾s 𝑘 ) ) )
25 24 15 eqeltrrd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( Base ‘ ( 𝐺 ↾s 𝑘 ) ) ∈ Fin )
26 eqid ⊢ ( Base ‘ ( 𝐺 ↾s 𝑘 ) ) = ( Base ‘ ( 𝐺 ↾s 𝑘 ) )
27 26 pgpfi ⊢ ( ( ( 𝐺 ↾s 𝑘 ) ∈ Grp ∧ ( Base ‘ ( 𝐺 ↾s 𝑘 ) ) ∈ Fin ) → ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ↔ ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝑘 ) ) ) = ( 𝑃 ↑ 𝑛 ) ) ) )
28 22 25 27 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ↔ ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝑘 ) ) ) = ( 𝑃 ↑ 𝑛 ) ) ) )
29 19 28 mpbid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝑘 ) ) ) = ( 𝑃 ↑ 𝑛 ) ) )
30 29 simpld ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝑃 ∈ ℙ )
31 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
32 30 31 syl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝑃 ∈ ℕ )
33 32 nnred ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝑃 ∈ ℝ )
34 32 nnge1d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 1 ≤ 𝑃 )
35 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
36 35 subg0cl ⊢ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑘 )
37 12 36 syl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( 0g ‘ 𝐺 ) ∈ 𝑘 )
38 37 ne0d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝑘 ≠ ∅ )
39 hashnncl ⊢ ( 𝑘 ∈ Fin → ( ( ♯ ‘ 𝑘 ) ∈ ℕ ↔ 𝑘 ≠ ∅ ) )
40 15 39 syl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ( ♯ ‘ 𝑘 ) ∈ ℕ ↔ 𝑘 ≠ ∅ ) )
41 38 40 mpbird ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ♯ ‘ 𝑘 ) ∈ ℕ )
42 30 41 pccld ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑘 ) ) ∈ ℕ0 )
43 42 nn0zd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑘 ) ) ∈ ℤ )
44 simpl1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝐺 ∈ Grp )
45 1 grpbn0 ⊢ ( 𝐺 ∈ Grp → 𝑋 ≠ ∅ )
46 44 45 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝑋 ≠ ∅ )
47 hashnncl ⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
48 10 47 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
49 46 48 mpbird ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ( ♯ ‘ 𝑋 ) ∈ ℕ )
50 8 49 pccld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℕ0 )
51 50 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℕ0 )
52 51 nn0zd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℤ )
53 oveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 pCnt ( ♯ ‘ 𝑘 ) ) = ( 𝑃 pCnt ( ♯ ‘ 𝑘 ) ) )
54 oveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) = ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) )
55 53 54 breq12d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 pCnt ( ♯ ‘ 𝑘 ) ) ≤ ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) ↔ ( 𝑃 pCnt ( ♯ ‘ 𝑘 ) ) ≤ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
56 1 lagsubg ⊢ ( ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑘 ) ∥ ( ♯ ‘ 𝑋 ) )
57 12 11 56 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ♯ ‘ 𝑘 ) ∥ ( ♯ ‘ 𝑋 ) )
58 41 nnzd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ♯ ‘ 𝑘 ) ∈ ℤ )
59 49 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ♯ ‘ 𝑋 ) ∈ ℕ )
60 59 nnzd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ♯ ‘ 𝑋 ) ∈ ℤ )
61 pc2dvds ⊢ ( ( ( ♯ ‘ 𝑘 ) ∈ ℤ ∧ ( ♯ ‘ 𝑋 ) ∈ ℤ ) → ( ( ♯ ‘ 𝑘 ) ∥ ( ♯ ‘ 𝑋 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ♯ ‘ 𝑘 ) ) ≤ ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) ) )
62 58 60 61 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ( ♯ ‘ 𝑘 ) ∥ ( ♯ ‘ 𝑋 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ♯ ‘ 𝑘 ) ) ≤ ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) ) )
63 57 62 mpbid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ♯ ‘ 𝑘 ) ) ≤ ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) )
64 55 63 30 rspcdva ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑘 ) ) ≤ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) )
65 eluz2 ⊢ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ( ℤ≥ ‘ ( 𝑃 pCnt ( ♯ ‘ 𝑘 ) ) ) ↔ ( ( 𝑃 pCnt ( ♯ ‘ 𝑘 ) ) ∈ ℤ ∧ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℤ ∧ ( 𝑃 pCnt ( ♯ ‘ 𝑘 ) ) ≤ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
66 43 52 64 65 syl3anbrc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ( ℤ≥ ‘ ( 𝑃 pCnt ( ♯ ‘ 𝑘 ) ) ) )
67 33 34 66 leexp2ad ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑘 ) ) ) ≤ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
68 29 simprd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝑘 ) ) ) = ( 𝑃 ↑ 𝑛 ) )
69 24 fveqeq2d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ 𝑛 ) ↔ ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝑘 ) ) ) = ( 𝑃 ↑ 𝑛 ) ) )
70 69 rexbidv ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝑘 ) ) ) = ( 𝑃 ↑ 𝑛 ) ) )
71 68 70 mpbird ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ 𝑛 ) )
72 pcprmpw ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝑘 ) ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ 𝑛 ) ↔ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑘 ) ) ) ) )
73 30 41 72 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ 𝑛 ) ↔ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑘 ) ) ) ) )
74 71 73 mpbid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑘 ) ) ) )
75 simplrr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
76 67 74 75 3brtr4d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ♯ ‘ 𝑘 ) ≤ ( ♯ ‘ 𝐻 ) )
77 1 subgss ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ⊆ 𝑋 )
78 77 ad2antrl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝐻 ⊆ 𝑋 )
79 10 78 ssfid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝐻 ∈ Fin )
80 79 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝐻 ∈ Fin )
81 hashdom ⊢ ( ( 𝑘 ∈ Fin ∧ 𝐻 ∈ Fin ) → ( ( ♯ ‘ 𝑘 ) ≤ ( ♯ ‘ 𝐻 ) ↔ 𝑘 ≼ 𝐻 ) )
82 15 80 81 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → ( ( ♯ ‘ 𝑘 ) ≤ ( ♯ ‘ 𝐻 ) ↔ 𝑘 ≼ 𝐻 ) )
83 76 82 mpbid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝑘 ≼ 𝐻 )
84 sbth ⊢ ( ( 𝐻 ≼ 𝑘 ∧ 𝑘 ≼ 𝐻 ) → 𝐻 ≈ 𝑘 )
85 18 83 84 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝐻 ≈ 𝑘 )
86 fisseneq ⊢ ( ( 𝑘 ∈ Fin ∧ 𝐻 ⊆ 𝑘 ∧ 𝐻 ≈ 𝑘 ) → 𝐻 = 𝑘 )
87 15 16 85 86 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) ) → 𝐻 = 𝑘 )
88 87 expr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) → 𝐻 = 𝑘 ) )
89 eqid ⊢ ( 𝐺 ↾s 𝐻 ) = ( 𝐺 ↾s 𝐻 )
90 89 subgbas ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 = ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) )
91 90 ad2antrl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝐻 = ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) )
92 91 fveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ) )
93 simprr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
94 92 93 eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
95 oveq2 ⊢ ( 𝑛 = ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
96 95 rspceeqv ⊢ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℕ0 ∧ ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) → ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ) = ( 𝑃 ↑ 𝑛 ) )
97 50 94 96 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ) = ( 𝑃 ↑ 𝑛 ) )
98 89 subggrp ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ↾s 𝐻 ) ∈ Grp )
99 98 ad2antrl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ( 𝐺 ↾s 𝐻 ) ∈ Grp )
100 91 79 eqeltrrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∈ Fin )
101 eqid ⊢ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) = ( Base ‘ ( 𝐺 ↾s 𝐻 ) )
102 101 pgpfi ⊢ ( ( ( 𝐺 ↾s 𝐻 ) ∈ Grp ∧ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∈ Fin ) → ( 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) ↔ ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ) = ( 𝑃 ↑ 𝑛 ) ) ) )
103 99 100 102 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ( 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) ↔ ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ) = ( 𝑃 ↑ 𝑛 ) ) ) )
104 8 97 103 mpbir2and ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) )
105 104 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) )
106 oveq2 ⊢ ( 𝐻 = 𝑘 → ( 𝐺 ↾s 𝐻 ) = ( 𝐺 ↾s 𝑘 ) )
107 106 breq2d ⊢ ( 𝐻 = 𝑘 → ( 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) ↔ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) )
108 eqimss ⊢ ( 𝐻 = 𝑘 → 𝐻 ⊆ 𝑘 )
109 108 biantrurd ⊢ ( 𝐻 = 𝑘 → ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ↔ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) )
110 107 109 bitrd ⊢ ( 𝐻 = 𝑘 → ( 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) ↔ ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) )
111 105 110 syl5ibcom ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐻 = 𝑘 → ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) )
112 88 111 impbid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) )
113 112 ralrimiva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) )
114 isslw ⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) )
115 8 9 113 114 syl3anbrc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) )
116 7 115 impbida ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) )