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