Metamath Proof Explorer


Theorem pgpssslw

Description: Every P -subgroup is contained in a Sylow P -subgroup. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypotheses pgpssslw.1 𝑋 = ( Base ‘ 𝐺 )
pgpssslw.2 𝑆 = ( 𝐺s 𝐻 )
pgpssslw.3 𝐹 = ( 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ↦ ( ♯ ‘ 𝑥 ) )
Assertion pgpssslw ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ∃ 𝑘 ∈ ( 𝑃 pSyl 𝐺 ) 𝐻𝑘 )

Proof

Step Hyp Ref Expression
1 pgpssslw.1 𝑋 = ( Base ‘ 𝐺 )
2 pgpssslw.2 𝑆 = ( 𝐺s 𝐻 )
3 pgpssslw.3 𝐹 = ( 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ↦ ( ♯ ‘ 𝑥 ) )
4 simp2 ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → 𝑋 ∈ Fin )
5 elrabi ( 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } → 𝑥 ∈ ( SubGrp ‘ 𝐺 ) )
6 1 subgss ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) → 𝑥𝑋 )
7 5 6 syl ( 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } → 𝑥𝑋 )
8 ssfi ( ( 𝑋 ∈ Fin ∧ 𝑥𝑋 ) → 𝑥 ∈ Fin )
9 4 7 8 syl2an ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ) → 𝑥 ∈ Fin )
10 hashcl ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
11 9 10 syl ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
12 11 nn0zd ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ) → ( ♯ ‘ 𝑥 ) ∈ ℤ )
13 12 3 fmptd ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → 𝐹 : { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ⟶ ℤ )
14 13 frnd ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ran 𝐹 ⊆ ℤ )
15 fvex ( ♯ ‘ 𝑥 ) ∈ V
16 15 3 fnmpti 𝐹 Fn { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) }
17 eqimss2 ( 𝑦 = 𝐻𝐻𝑦 )
18 17 biantrud ( 𝑦 = 𝐻 → ( 𝑃 pGrp ( 𝐺s 𝑦 ) ↔ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) ) )
19 oveq2 ( 𝑦 = 𝐻 → ( 𝐺s 𝑦 ) = ( 𝐺s 𝐻 ) )
20 19 2 eqtr4di ( 𝑦 = 𝐻 → ( 𝐺s 𝑦 ) = 𝑆 )
21 20 breq2d ( 𝑦 = 𝐻 → ( 𝑃 pGrp ( 𝐺s 𝑦 ) ↔ 𝑃 pGrp 𝑆 ) )
22 18 21 bitr3d ( 𝑦 = 𝐻 → ( ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) ↔ 𝑃 pGrp 𝑆 ) )
23 simp1 ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
24 simp3 ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → 𝑃 pGrp 𝑆 )
25 22 23 24 elrabd ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → 𝐻 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } )
26 fnfvelrn ( ( 𝐹 Fn { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ∧ 𝐻 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ) → ( 𝐹𝐻 ) ∈ ran 𝐹 )
27 16 25 26 sylancr ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ( 𝐹𝐻 ) ∈ ran 𝐹 )
28 27 ne0d ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ran 𝐹 ≠ ∅ )
29 hashcl ( 𝑋 ∈ Fin → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
30 4 29 syl ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
31 30 nn0red ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ( ♯ ‘ 𝑋 ) ∈ ℝ )
32 fveq2 ( 𝑥 = 𝑚 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑚 ) )
33 fvex ( ♯ ‘ 𝑚 ) ∈ V
34 32 3 33 fvmpt ( 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } → ( 𝐹𝑚 ) = ( ♯ ‘ 𝑚 ) )
35 34 adantl ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ) → ( 𝐹𝑚 ) = ( ♯ ‘ 𝑚 ) )
36 oveq2 ( 𝑦 = 𝑚 → ( 𝐺s 𝑦 ) = ( 𝐺s 𝑚 ) )
37 36 breq2d ( 𝑦 = 𝑚 → ( 𝑃 pGrp ( 𝐺s 𝑦 ) ↔ 𝑃 pGrp ( 𝐺s 𝑚 ) ) )
38 sseq2 ( 𝑦 = 𝑚 → ( 𝐻𝑦𝐻𝑚 ) )
39 37 38 anbi12d ( 𝑦 = 𝑚 → ( ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) ↔ ( 𝑃 pGrp ( 𝐺s 𝑚 ) ∧ 𝐻𝑚 ) ) )
40 39 elrab ( 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ↔ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺s 𝑚 ) ∧ 𝐻𝑚 ) ) )
41 4 adantr ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺s 𝑚 ) ∧ 𝐻𝑚 ) ) ) → 𝑋 ∈ Fin )
42 1 subgss ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) → 𝑚𝑋 )
43 42 ad2antrl ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺s 𝑚 ) ∧ 𝐻𝑚 ) ) ) → 𝑚𝑋 )
44 ssdomg ( 𝑋 ∈ Fin → ( 𝑚𝑋𝑚𝑋 ) )
45 41 43 44 sylc ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺s 𝑚 ) ∧ 𝐻𝑚 ) ) ) → 𝑚𝑋 )
46 41 43 ssfid ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺s 𝑚 ) ∧ 𝐻𝑚 ) ) ) → 𝑚 ∈ Fin )
47 hashdom ( ( 𝑚 ∈ Fin ∧ 𝑋 ∈ Fin ) → ( ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑋 ) ↔ 𝑚𝑋 ) )
48 46 41 47 syl2anc ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺s 𝑚 ) ∧ 𝐻𝑚 ) ) ) → ( ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑋 ) ↔ 𝑚𝑋 ) )
49 45 48 mpbird ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺s 𝑚 ) ∧ 𝐻𝑚 ) ) ) → ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑋 ) )
50 40 49 sylan2b ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ) → ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑋 ) )
51 35 50 eqbrtrd ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ) → ( 𝐹𝑚 ) ≤ ( ♯ ‘ 𝑋 ) )
52 51 ralrimiva ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ∀ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ( 𝐹𝑚 ) ≤ ( ♯ ‘ 𝑋 ) )
53 breq1 ( 𝑤 = ( 𝐹𝑚 ) → ( 𝑤 ≤ ( ♯ ‘ 𝑋 ) ↔ ( 𝐹𝑚 ) ≤ ( ♯ ‘ 𝑋 ) ) )
54 53 ralrn ( 𝐹 Fn { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } → ( ∀ 𝑤 ∈ ran 𝐹 𝑤 ≤ ( ♯ ‘ 𝑋 ) ↔ ∀ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ( 𝐹𝑚 ) ≤ ( ♯ ‘ 𝑋 ) ) )
55 16 54 ax-mp ( ∀ 𝑤 ∈ ran 𝐹 𝑤 ≤ ( ♯ ‘ 𝑋 ) ↔ ∀ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ( 𝐹𝑚 ) ≤ ( ♯ ‘ 𝑋 ) )
56 52 55 sylibr ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ∀ 𝑤 ∈ ran 𝐹 𝑤 ≤ ( ♯ ‘ 𝑋 ) )
57 brralrspcev ( ( ( ♯ ‘ 𝑋 ) ∈ ℝ ∧ ∀ 𝑤 ∈ ran 𝐹 𝑤 ≤ ( ♯ ‘ 𝑋 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran 𝐹 𝑤𝑧 )
58 31 56 57 syl2anc ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran 𝐹 𝑤𝑧 )
59 suprzcl ( ( ran 𝐹 ⊆ ℤ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran 𝐹 𝑤𝑧 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
60 14 28 58 59 syl3anc ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
61 fvelrnb ( 𝐹 Fn { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } → ( sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ↔ ∃ 𝑘 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) )
62 16 61 ax-mp ( sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ↔ ∃ 𝑘 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) )
63 60 62 sylib ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ∃ 𝑘 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) )
64 oveq2 ( 𝑦 = 𝑘 → ( 𝐺s 𝑦 ) = ( 𝐺s 𝑘 ) )
65 64 breq2d ( 𝑦 = 𝑘 → ( 𝑃 pGrp ( 𝐺s 𝑦 ) ↔ 𝑃 pGrp ( 𝐺s 𝑘 ) ) )
66 sseq2 ( 𝑦 = 𝑘 → ( 𝐻𝑦𝐻𝑘 ) )
67 65 66 anbi12d ( 𝑦 = 𝑘 → ( ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) ↔ ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ) )
68 67 rexrab ( ∃ 𝑘 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ↔ ∃ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) )
69 63 68 sylib ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ∃ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) )
70 simpl3 ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → 𝑃 pGrp 𝑆 )
71 pgpprm ( 𝑃 pGrp 𝑆𝑃 ∈ ℙ )
72 70 71 syl ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → 𝑃 ∈ ℙ )
73 simprl ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → 𝑘 ∈ ( SubGrp ‘ 𝐺 ) )
74 zssre ℤ ⊆ ℝ
75 14 74 sstrdi ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ran 𝐹 ⊆ ℝ )
76 75 ad2antrr ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ran 𝐹 ⊆ ℝ )
77 28 ad2antrr ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ran 𝐹 ≠ ∅ )
78 58 ad2antrr ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran 𝐹 𝑤𝑧 )
79 simprl ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → 𝑚 ∈ ( SubGrp ‘ 𝐺 ) )
80 simprrr ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → 𝑃 pGrp ( 𝐺s 𝑚 ) )
81 simprrl ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) )
82 81 adantr ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) )
83 82 simprd ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → 𝐻𝑘 )
84 simprrl ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → 𝑘𝑚 )
85 83 84 sstrd ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → 𝐻𝑚 )
86 80 85 jca ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( 𝑃 pGrp ( 𝐺s 𝑚 ) ∧ 𝐻𝑚 ) )
87 39 79 86 elrabd ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } )
88 87 34 syl ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( 𝐹𝑚 ) = ( ♯ ‘ 𝑚 ) )
89 fnfvelrn ( ( 𝐹 Fn { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ∧ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } ) → ( 𝐹𝑚 ) ∈ ran 𝐹 )
90 16 87 89 sylancr ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( 𝐹𝑚 ) ∈ ran 𝐹 )
91 88 90 eqeltrrd ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( ♯ ‘ 𝑚 ) ∈ ran 𝐹 )
92 76 77 78 91 suprubd ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( ♯ ‘ 𝑚 ) ≤ sup ( ran 𝐹 , ℝ , < ) )
93 simprrr ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) )
94 93 adantr ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) )
95 73 adantr ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → 𝑘 ∈ ( SubGrp ‘ 𝐺 ) )
96 67 95 82 elrabd ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → 𝑘 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } )
97 fveq2 ( 𝑥 = 𝑘 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑘 ) )
98 fvex ( ♯ ‘ 𝑘 ) ∈ V
99 97 3 98 fvmpt ( 𝑘 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺s 𝑦 ) ∧ 𝐻𝑦 ) } → ( 𝐹𝑘 ) = ( ♯ ‘ 𝑘 ) )
100 96 99 syl ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( 𝐹𝑘 ) = ( ♯ ‘ 𝑘 ) )
101 94 100 eqtr3d ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → sup ( ran 𝐹 , ℝ , < ) = ( ♯ ‘ 𝑘 ) )
102 92 101 breqtrd ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑘 ) )
103 simpll2 ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → 𝑋 ∈ Fin )
104 42 ad2antrl ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → 𝑚𝑋 )
105 103 104 ssfid ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → 𝑚 ∈ Fin )
106 105 84 ssfid ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → 𝑘 ∈ Fin )
107 hashcl ( 𝑚 ∈ Fin → ( ♯ ‘ 𝑚 ) ∈ ℕ0 )
108 hashcl ( 𝑘 ∈ Fin → ( ♯ ‘ 𝑘 ) ∈ ℕ0 )
109 nn0re ( ( ♯ ‘ 𝑚 ) ∈ ℕ0 → ( ♯ ‘ 𝑚 ) ∈ ℝ )
110 nn0re ( ( ♯ ‘ 𝑘 ) ∈ ℕ0 → ( ♯ ‘ 𝑘 ) ∈ ℝ )
111 lenlt ( ( ( ♯ ‘ 𝑚 ) ∈ ℝ ∧ ( ♯ ‘ 𝑘 ) ∈ ℝ ) → ( ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑘 ) ↔ ¬ ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ) )
112 109 110 111 syl2an ( ( ( ♯ ‘ 𝑚 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑘 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑘 ) ↔ ¬ ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ) )
113 107 108 112 syl2an ( ( 𝑚 ∈ Fin ∧ 𝑘 ∈ Fin ) → ( ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑘 ) ↔ ¬ ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ) )
114 105 106 113 syl2anc ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑘 ) ↔ ¬ ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ) )
115 102 114 mpbid ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ¬ ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) )
116 php3 ( ( 𝑚 ∈ Fin ∧ 𝑘𝑚 ) → 𝑘𝑚 )
117 116 ex ( 𝑚 ∈ Fin → ( 𝑘𝑚𝑘𝑚 ) )
118 105 117 syl ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( 𝑘𝑚𝑘𝑚 ) )
119 hashsdom ( ( 𝑘 ∈ Fin ∧ 𝑚 ∈ Fin ) → ( ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ↔ 𝑘𝑚 ) )
120 106 105 119 syl2anc ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ↔ 𝑘𝑚 ) )
121 118 120 sylibrd ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( 𝑘𝑚 → ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ) )
122 115 121 mtod ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ¬ 𝑘𝑚 )
123 sspss ( 𝑘𝑚 ↔ ( 𝑘𝑚𝑘 = 𝑚 ) )
124 84 123 sylib ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( 𝑘𝑚𝑘 = 𝑚 ) )
125 124 ord ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → ( ¬ 𝑘𝑚𝑘 = 𝑚 ) )
126 122 125 mpd ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) ) → 𝑘 = 𝑚 )
127 126 expr ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) → 𝑘 = 𝑚 ) )
128 81 simpld ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → 𝑃 pGrp ( 𝐺s 𝑘 ) )
129 128 adantr ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑃 pGrp ( 𝐺s 𝑘 ) )
130 oveq2 ( 𝑘 = 𝑚 → ( 𝐺s 𝑘 ) = ( 𝐺s 𝑚 ) )
131 130 breq2d ( 𝑘 = 𝑚 → ( 𝑃 pGrp ( 𝐺s 𝑘 ) ↔ 𝑃 pGrp ( 𝐺s 𝑚 ) ) )
132 eqimss ( 𝑘 = 𝑚𝑘𝑚 )
133 132 biantrurd ( 𝑘 = 𝑚 → ( 𝑃 pGrp ( 𝐺s 𝑚 ) ↔ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) )
134 131 133 bitrd ( 𝑘 = 𝑚 → ( 𝑃 pGrp ( 𝐺s 𝑘 ) ↔ ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) )
135 129 134 syl5ibcom ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑘 = 𝑚 → ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ) )
136 127 135 impbid ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ↔ 𝑘 = 𝑚 ) )
137 136 ralrimiva ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → ∀ 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ↔ 𝑘 = 𝑚 ) )
138 isslw ( 𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑘𝑚𝑃 pGrp ( 𝐺s 𝑚 ) ) ↔ 𝑘 = 𝑚 ) ) )
139 72 73 137 138 syl3anbrc ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → 𝑘 ∈ ( 𝑃 pSyl 𝐺 ) )
140 81 simprd ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺s 𝑘 ) ∧ 𝐻𝑘 ) ∧ ( 𝐹𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → 𝐻𝑘 )
141 69 139 140 reximssdv ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ∃ 𝑘 ∈ ( 𝑃 pSyl 𝐺 ) 𝐻𝑘 )