MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pgpssslw Structured version   Visualization version   GIF version

Theorem pgpssslw 18227
Description: Every 𝑃-subgroup is contained in a Sylow 𝑃-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.)
Hypotheses
Ref Expression
pgpssslw.1 𝑋 = (Base‘𝐺)
pgpssslw.2 𝑆 = (𝐺s 𝐻)
pgpssslw.3 𝐹 = (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} ↦ (♯‘𝑥))
Assertion
Ref Expression
pgpssslw ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ (𝑃 pSyl 𝐺)𝐻𝑘)
Distinct variable groups:   𝑥,𝑘,𝑦,𝐺   𝑘,𝐻,𝑥,𝑦   𝑃,𝑘,𝑥,𝑦   𝑘,𝑋,𝑥   𝑘,𝐹   𝑆,𝑘,𝑥,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦)   𝑋(𝑦)

Proof of Theorem pgpssslw
Dummy variables 𝑚 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2 1132 . . . . . . . . . 10 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝑋 ∈ Fin)
2 elrabi 3497 . . . . . . . . . . 11 (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} → 𝑥 ∈ (SubGrp‘𝐺))
3 pgpssslw.1 . . . . . . . . . . . 12 𝑋 = (Base‘𝐺)
43subgss 17794 . . . . . . . . . . 11 (𝑥 ∈ (SubGrp‘𝐺) → 𝑥𝑋)
52, 4syl 17 . . . . . . . . . 10 (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} → 𝑥𝑋)
6 ssfi 8343 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝑥𝑋) → 𝑥 ∈ Fin)
71, 5, 6syl2an 495 . . . . . . . . 9 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → 𝑥 ∈ Fin)
8 hashcl 13337 . . . . . . . . 9 (𝑥 ∈ Fin → (♯‘𝑥) ∈ ℕ0)
97, 8syl 17 . . . . . . . 8 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (♯‘𝑥) ∈ ℕ0)
109nn0zd 11670 . . . . . . 7 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (♯‘𝑥) ∈ ℤ)
11 pgpssslw.3 . . . . . . 7 𝐹 = (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} ↦ (♯‘𝑥))
1210, 11fmptd 6546 . . . . . 6 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝐹:{𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}⟶ℤ)
13 frn 6212 . . . . . 6 (𝐹:{𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}⟶ℤ → ran 𝐹 ⊆ ℤ)
1412, 13syl 17 . . . . 5 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ran 𝐹 ⊆ ℤ)
15 fvex 6360 . . . . . . . 8 (♯‘𝑥) ∈ V
1615, 11fnmpti 6181 . . . . . . 7 𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}
17 simp1 1131 . . . . . . . 8 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝐻 ∈ (SubGrp‘𝐺))
18 simp3 1133 . . . . . . . 8 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝑃 pGrp 𝑆)
19 eqimss2 3797 . . . . . . . . . . 11 (𝑦 = 𝐻𝐻𝑦)
2019biantrud 529 . . . . . . . . . 10 (𝑦 = 𝐻 → (𝑃 pGrp (𝐺s 𝑦) ↔ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)))
21 oveq2 6819 . . . . . . . . . . . 12 (𝑦 = 𝐻 → (𝐺s 𝑦) = (𝐺s 𝐻))
22 pgpssslw.2 . . . . . . . . . . . 12 𝑆 = (𝐺s 𝐻)
2321, 22syl6eqr 2810 . . . . . . . . . . 11 (𝑦 = 𝐻 → (𝐺s 𝑦) = 𝑆)
2423breq2d 4814 . . . . . . . . . 10 (𝑦 = 𝐻 → (𝑃 pGrp (𝐺s 𝑦) ↔ 𝑃 pGrp 𝑆))
2520, 24bitr3d 270 . . . . . . . . 9 (𝑦 = 𝐻 → ((𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦) ↔ 𝑃 pGrp 𝑆))
2625elrab 3502 . . . . . . . 8 (𝐻 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} ↔ (𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑃 pGrp 𝑆))
2717, 18, 26sylanbrc 701 . . . . . . 7 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝐻 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)})
28 fnfvelrn 6517 . . . . . . 7 ((𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} ∧ 𝐻 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (𝐹𝐻) ∈ ran 𝐹)
2916, 27, 28sylancr 698 . . . . . 6 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (𝐹𝐻) ∈ ran 𝐹)
30 ne0i 4062 . . . . . 6 ((𝐹𝐻) ∈ ran 𝐹 → ran 𝐹 ≠ ∅)
3129, 30syl 17 . . . . 5 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ran 𝐹 ≠ ∅)
32 hashcl 13337 . . . . . . . 8 (𝑋 ∈ Fin → (♯‘𝑋) ∈ ℕ0)
331, 32syl 17 . . . . . . 7 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (♯‘𝑋) ∈ ℕ0)
3433nn0red 11542 . . . . . 6 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (♯‘𝑋) ∈ ℝ)
35 fveq2 6350 . . . . . . . . . . 11 (𝑥 = 𝑚 → (♯‘𝑥) = (♯‘𝑚))
36 fvex 6360 . . . . . . . . . . 11 (♯‘𝑚) ∈ V
3735, 11, 36fvmpt 6442 . . . . . . . . . 10 (𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} → (𝐹𝑚) = (♯‘𝑚))
3837adantl 473 . . . . . . . . 9 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (𝐹𝑚) = (♯‘𝑚))
39 oveq2 6819 . . . . . . . . . . . . 13 (𝑦 = 𝑚 → (𝐺s 𝑦) = (𝐺s 𝑚))
4039breq2d 4814 . . . . . . . . . . . 12 (𝑦 = 𝑚 → (𝑃 pGrp (𝐺s 𝑦) ↔ 𝑃 pGrp (𝐺s 𝑚)))
41 sseq2 3766 . . . . . . . . . . . 12 (𝑦 = 𝑚 → (𝐻𝑦𝐻𝑚))
4240, 41anbi12d 749 . . . . . . . . . . 11 (𝑦 = 𝑚 → ((𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦) ↔ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚)))
4342elrab 3502 . . . . . . . . . 10 (𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} ↔ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚)))
441adantr 472 . . . . . . . . . . . 12 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))) → 𝑋 ∈ Fin)
453subgss 17794 . . . . . . . . . . . . 13 (𝑚 ∈ (SubGrp‘𝐺) → 𝑚𝑋)
4645ad2antrl 766 . . . . . . . . . . . 12 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))) → 𝑚𝑋)
47 ssdomg 8165 . . . . . . . . . . . 12 (𝑋 ∈ Fin → (𝑚𝑋𝑚𝑋))
4844, 46, 47sylc 65 . . . . . . . . . . 11 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))) → 𝑚𝑋)
49 ssfi 8343 . . . . . . . . . . . . 13 ((𝑋 ∈ Fin ∧ 𝑚𝑋) → 𝑚 ∈ Fin)
5044, 46, 49syl2anc 696 . . . . . . . . . . . 12 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))) → 𝑚 ∈ Fin)
51 hashdom 13358 . . . . . . . . . . . 12 ((𝑚 ∈ Fin ∧ 𝑋 ∈ Fin) → ((♯‘𝑚) ≤ (♯‘𝑋) ↔ 𝑚𝑋))
5250, 44, 51syl2anc 696 . . . . . . . . . . 11 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))) → ((♯‘𝑚) ≤ (♯‘𝑋) ↔ 𝑚𝑋))
5348, 52mpbird 247 . . . . . . . . . 10 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))) → (♯‘𝑚) ≤ (♯‘𝑋))
5443, 53sylan2b 493 . . . . . . . . 9 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (♯‘𝑚) ≤ (♯‘𝑋))
5538, 54eqbrtrd 4824 . . . . . . . 8 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (𝐹𝑚) ≤ (♯‘𝑋))
5655ralrimiva 3102 . . . . . . 7 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∀𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑚) ≤ (♯‘𝑋))
57 breq1 4805 . . . . . . . . 9 (𝑤 = (𝐹𝑚) → (𝑤 ≤ (♯‘𝑋) ↔ (𝐹𝑚) ≤ (♯‘𝑋)))
5857ralrn 6523 . . . . . . . 8 (𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} → (∀𝑤 ∈ ran 𝐹 𝑤 ≤ (♯‘𝑋) ↔ ∀𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑚) ≤ (♯‘𝑋)))
5916, 58ax-mp 5 . . . . . . 7 (∀𝑤 ∈ ran 𝐹 𝑤 ≤ (♯‘𝑋) ↔ ∀𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑚) ≤ (♯‘𝑋))
6056, 59sylibr 224 . . . . . 6 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∀𝑤 ∈ ran 𝐹 𝑤 ≤ (♯‘𝑋))
61 breq2 4806 . . . . . . . 8 (𝑧 = (♯‘𝑋) → (𝑤𝑧𝑤 ≤ (♯‘𝑋)))
6261ralbidv 3122 . . . . . . 7 (𝑧 = (♯‘𝑋) → (∀𝑤 ∈ ran 𝐹 𝑤𝑧 ↔ ∀𝑤 ∈ ran 𝐹 𝑤 ≤ (♯‘𝑋)))
6362rspcev 3447 . . . . . 6 (((♯‘𝑋) ∈ ℝ ∧ ∀𝑤 ∈ ran 𝐹 𝑤 ≤ (♯‘𝑋)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤𝑧)
6434, 60, 63syl2anc 696 . . . . 5 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤𝑧)
65 suprzcl 11647 . . . . 5 ((ran 𝐹 ⊆ ℤ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤𝑧) → sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹)
6614, 31, 64, 65syl3anc 1477 . . . 4 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹)
67 fvelrnb 6403 . . . . 5 (𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} → (sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ↔ ∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))
6816, 67ax-mp 5 . . . 4 (sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ↔ ∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑘) = sup(ran 𝐹, ℝ, < ))
6966, 68sylib 208 . . 3 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑘) = sup(ran 𝐹, ℝ, < ))
70 oveq2 6819 . . . . . 6 (𝑦 = 𝑘 → (𝐺s 𝑦) = (𝐺s 𝑘))
7170breq2d 4814 . . . . 5 (𝑦 = 𝑘 → (𝑃 pGrp (𝐺s 𝑦) ↔ 𝑃 pGrp (𝐺s 𝑘)))
72 sseq2 3766 . . . . 5 (𝑦 = 𝑘 → (𝐻𝑦𝐻𝑘))
7371, 72anbi12d 749 . . . 4 (𝑦 = 𝑘 → ((𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦) ↔ (𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘)))
7473rexrab 3509 . . 3 (∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑘) = sup(ran 𝐹, ℝ, < ) ↔ ∃𝑘 ∈ (SubGrp‘𝐺)((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))
7569, 74sylib 208 . 2 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ (SubGrp‘𝐺)((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))
76 simpl3 1232 . . . . . . 7 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑃 pGrp 𝑆)
77 pgpprm 18206 . . . . . . 7 (𝑃 pGrp 𝑆𝑃 ∈ ℙ)
7876, 77syl 17 . . . . . 6 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑃 ∈ ℙ)
79 simprl 811 . . . . . 6 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑘 ∈ (SubGrp‘𝐺))
80 zssre 11574 . . . . . . . . . . . . . . . 16 ℤ ⊆ ℝ
8114, 80syl6ss 3754 . . . . . . . . . . . . . . 15 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ran 𝐹 ⊆ ℝ)
8281ad2antrr 764 . . . . . . . . . . . . . 14 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ran 𝐹 ⊆ ℝ)
8331ad2antrr 764 . . . . . . . . . . . . . 14 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ran 𝐹 ≠ ∅)
8464ad2antrr 764 . . . . . . . . . . . . . 14 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤𝑧)
85 simprl 811 . . . . . . . . . . . . . . . . 17 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑚 ∈ (SubGrp‘𝐺))
86 simprrr 824 . . . . . . . . . . . . . . . . . 18 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑃 pGrp (𝐺s 𝑚))
87 simprrl 823 . . . . . . . . . . . . . . . . . . . . 21 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → (𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘))
8887adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘))
8988simprd 482 . . . . . . . . . . . . . . . . . . 19 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝐻𝑘)
90 simprrl 823 . . . . . . . . . . . . . . . . . . 19 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑘𝑚)
9189, 90sstrd 3752 . . . . . . . . . . . . . . . . . 18 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝐻𝑚)
9286, 91jca 555 . . . . . . . . . . . . . . . . 17 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))
9385, 92, 43sylanbrc 701 . . . . . . . . . . . . . . . 16 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)})
9493, 37syl 17 . . . . . . . . . . . . . . 15 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝐹𝑚) = (♯‘𝑚))
95 fnfvelrn 6517 . . . . . . . . . . . . . . . 16 ((𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (𝐹𝑚) ∈ ran 𝐹)
9616, 93, 95sylancr 698 . . . . . . . . . . . . . . 15 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝐹𝑚) ∈ ran 𝐹)
9794, 96eqeltrrd 2838 . . . . . . . . . . . . . 14 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (♯‘𝑚) ∈ ran 𝐹)
98 suprub 11174 . . . . . . . . . . . . . 14 (((ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤𝑧) ∧ (♯‘𝑚) ∈ ran 𝐹) → (♯‘𝑚) ≤ sup(ran 𝐹, ℝ, < ))
9982, 83, 84, 97, 98syl31anc 1480 . . . . . . . . . . . . 13 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (♯‘𝑚) ≤ sup(ran 𝐹, ℝ, < ))
100 simprrr 824 . . . . . . . . . . . . . . 15 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → (𝐹𝑘) = sup(ran 𝐹, ℝ, < ))
101100adantr 472 . . . . . . . . . . . . . 14 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝐹𝑘) = sup(ran 𝐹, ℝ, < ))
10279adantr 472 . . . . . . . . . . . . . . . 16 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑘 ∈ (SubGrp‘𝐺))
10373elrab 3502 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} ↔ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘)))
104102, 88, 103sylanbrc 701 . . . . . . . . . . . . . . 15 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)})
105 fveq2 6350 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑘 → (♯‘𝑥) = (♯‘𝑘))
106 fvex 6360 . . . . . . . . . . . . . . . 16 (♯‘𝑘) ∈ V
107105, 11, 106fvmpt 6442 . . . . . . . . . . . . . . 15 (𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} → (𝐹𝑘) = (♯‘𝑘))
108104, 107syl 17 . . . . . . . . . . . . . 14 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝐹𝑘) = (♯‘𝑘))
109101, 108eqtr3d 2794 . . . . . . . . . . . . 13 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → sup(ran 𝐹, ℝ, < ) = (♯‘𝑘))
11099, 109breqtrd 4828 . . . . . . . . . . . 12 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (♯‘𝑚) ≤ (♯‘𝑘))
111 simpll2 1257 . . . . . . . . . . . . . 14 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑋 ∈ Fin)
11245ad2antrl 766 . . . . . . . . . . . . . 14 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑚𝑋)
113111, 112, 49syl2anc 696 . . . . . . . . . . . . 13 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑚 ∈ Fin)
114 ssfi 8343 . . . . . . . . . . . . . 14 ((𝑚 ∈ Fin ∧ 𝑘𝑚) → 𝑘 ∈ Fin)
115113, 90, 114syl2anc 696 . . . . . . . . . . . . 13 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑘 ∈ Fin)
116 hashcl 13337 . . . . . . . . . . . . . 14 (𝑚 ∈ Fin → (♯‘𝑚) ∈ ℕ0)
117 hashcl 13337 . . . . . . . . . . . . . 14 (𝑘 ∈ Fin → (♯‘𝑘) ∈ ℕ0)
118 nn0re 11491 . . . . . . . . . . . . . . 15 ((♯‘𝑚) ∈ ℕ0 → (♯‘𝑚) ∈ ℝ)
119 nn0re 11491 . . . . . . . . . . . . . . 15 ((♯‘𝑘) ∈ ℕ0 → (♯‘𝑘) ∈ ℝ)
120 lenlt 10306 . . . . . . . . . . . . . . 15 (((♯‘𝑚) ∈ ℝ ∧ (♯‘𝑘) ∈ ℝ) → ((♯‘𝑚) ≤ (♯‘𝑘) ↔ ¬ (♯‘𝑘) < (♯‘𝑚)))
121118, 119, 120syl2an 495 . . . . . . . . . . . . . 14 (((♯‘𝑚) ∈ ℕ0 ∧ (♯‘𝑘) ∈ ℕ0) → ((♯‘𝑚) ≤ (♯‘𝑘) ↔ ¬ (♯‘𝑘) < (♯‘𝑚)))
122116, 117, 121syl2an 495 . . . . . . . . . . . . 13 ((𝑚 ∈ Fin ∧ 𝑘 ∈ Fin) → ((♯‘𝑚) ≤ (♯‘𝑘) ↔ ¬ (♯‘𝑘) < (♯‘𝑚)))
123113, 115, 122syl2anc 696 . . . . . . . . . . . 12 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ((♯‘𝑚) ≤ (♯‘𝑘) ↔ ¬ (♯‘𝑘) < (♯‘𝑚)))
124110, 123mpbid 222 . . . . . . . . . . 11 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ¬ (♯‘𝑘) < (♯‘𝑚))
125 php3 8309 . . . . . . . . . . . . . 14 ((𝑚 ∈ Fin ∧ 𝑘𝑚) → 𝑘𝑚)
126125ex 449 . . . . . . . . . . . . 13 (𝑚 ∈ Fin → (𝑘𝑚𝑘𝑚))
127113, 126syl 17 . . . . . . . . . . . 12 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝑘𝑚𝑘𝑚))
128 hashsdom 13360 . . . . . . . . . . . . 13 ((𝑘 ∈ Fin ∧ 𝑚 ∈ Fin) → ((♯‘𝑘) < (♯‘𝑚) ↔ 𝑘𝑚))
129115, 113, 128syl2anc 696 . . . . . . . . . . . 12 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ((♯‘𝑘) < (♯‘𝑚) ↔ 𝑘𝑚))
130127, 129sylibrd 249 . . . . . . . . . . 11 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝑘𝑚 → (♯‘𝑘) < (♯‘𝑚)))
131124, 130mtod 189 . . . . . . . . . 10 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ¬ 𝑘𝑚)
132 sspss 3846 . . . . . . . . . . . 12 (𝑘𝑚 ↔ (𝑘𝑚𝑘 = 𝑚))
13390, 132sylib 208 . . . . . . . . . . 11 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝑘𝑚𝑘 = 𝑚))
134133ord 391 . . . . . . . . . 10 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (¬ 𝑘𝑚𝑘 = 𝑚))
135131, 134mpd 15 . . . . . . . . 9 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑘 = 𝑚)
136135expr 644 . . . . . . . 8 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → ((𝑘𝑚𝑃 pGrp (𝐺s 𝑚)) → 𝑘 = 𝑚))
13787simpld 477 . . . . . . . . . 10 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑃 pGrp (𝐺s 𝑘))
138137adantr 472 . . . . . . . . 9 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺s 𝑘))
139 oveq2 6819 . . . . . . . . . . 11 (𝑘 = 𝑚 → (𝐺s 𝑘) = (𝐺s 𝑚))
140139breq2d 4814 . . . . . . . . . 10 (𝑘 = 𝑚 → (𝑃 pGrp (𝐺s 𝑘) ↔ 𝑃 pGrp (𝐺s 𝑚)))
141 eqimss 3796 . . . . . . . . . . 11 (𝑘 = 𝑚𝑘𝑚)
142141biantrurd 530 . . . . . . . . . 10 (𝑘 = 𝑚 → (𝑃 pGrp (𝐺s 𝑚) ↔ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚))))
143140, 142bitrd 268 . . . . . . . . 9 (𝑘 = 𝑚 → (𝑃 pGrp (𝐺s 𝑘) ↔ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚))))
144138, 143syl5ibcom 235 . . . . . . . 8 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → (𝑘 = 𝑚 → (𝑘𝑚𝑃 pGrp (𝐺s 𝑚))))
145136, 144impbid 202 . . . . . . 7 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → ((𝑘𝑚𝑃 pGrp (𝐺s 𝑚)) ↔ 𝑘 = 𝑚))
146145ralrimiva 3102 . . . . . 6 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → ∀𝑚 ∈ (SubGrp‘𝐺)((𝑘𝑚𝑃 pGrp (𝐺s 𝑚)) ↔ 𝑘 = 𝑚))
147 isslw 18221 . . . . . 6 (𝑘 ∈ (𝑃 pSyl 𝐺) ↔ (𝑃 ∈ ℙ ∧ 𝑘 ∈ (SubGrp‘𝐺) ∧ ∀𝑚 ∈ (SubGrp‘𝐺)((𝑘𝑚𝑃 pGrp (𝐺s 𝑚)) ↔ 𝑘 = 𝑚)))
14878, 79, 146, 147syl3anbrc 1429 . . . . 5 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑘 ∈ (𝑃 pSyl 𝐺))
14987simprd 482 . . . . 5 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝐻𝑘)
150148, 149jca 555 . . . 4 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → (𝑘 ∈ (𝑃 pSyl 𝐺) ∧ 𝐻𝑘))
151150ex 449 . . 3 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ((𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < ))) → (𝑘 ∈ (𝑃 pSyl 𝐺) ∧ 𝐻𝑘)))
152151reximdv2 3150 . 2 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (∃𝑘 ∈ (SubGrp‘𝐺)((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )) → ∃𝑘 ∈ (𝑃 pSyl 𝐺)𝐻𝑘))
15375, 152mpd 15 1 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ (𝑃 pSyl 𝐺)𝐻𝑘)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1630  wcel 2137  wne 2930  wral 3048  wrex 3049  {crab 3052  wss 3713  wpss 3714  c0 4056   class class class wbr 4802  cmpt 4879  ran crn 5265   Fn wfn 6042  wf 6043  cfv 6047  (class class class)co 6811  cdom 8117  csdm 8118  Fincfn 8119  supcsup 8509  cr 10125   < clt 10264  cle 10265  0cn0 11482  cz 11567  chash 13309  cprime 15585  Basecbs 16057  s cress 16058  SubGrpcsubg 17787   pGrp cpgp 18144   pSyl cslw 18145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203  ax-pre-sup 10204
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-int 4626  df-iun 4672  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-om 7229  df-1st 7331  df-2nd 7332  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-1o 7727  df-oadd 7731  df-er 7909  df-en 8120  df-dom 8121  df-sdom 8122  df-fin 8123  df-sup 8511  df-card 8953  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-nn 11211  df-n0 11483  df-xnn0 11554  df-z 11568  df-uz 11878  df-fz 12518  df-hash 13310  df-subg 17790  df-pgp 18148  df-slw 18149
This theorem is referenced by:  slwn0  18228
  Copyright terms: Public domain W3C validator