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 𝐺 ) 𝐻 ⊆ 𝑘 )