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

Theorem pgpssslw 18295
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 1167 . . . . . . . . . 10 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝑋 ∈ Fin)
2 elrabi 3514 . . . . . . . . . . 11 (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} → 𝑥 ∈ (SubGrp‘𝐺))
3 pgpssslw.1 . . . . . . . . . . . 12 𝑋 = (Base‘𝐺)
43subgss 17861 . . . . . . . . . . 11 (𝑥 ∈ (SubGrp‘𝐺) → 𝑥𝑋)
52, 4syl 17 . . . . . . . . . 10 (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} → 𝑥𝑋)
6 ssfi 8387 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝑥𝑋) → 𝑥 ∈ Fin)
71, 5, 6syl2an 589 . . . . . . . . 9 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → 𝑥 ∈ Fin)
8 hashcl 13349 . . . . . . . . 9 (𝑥 ∈ Fin → (♯‘𝑥) ∈ ℕ0)
97, 8syl 17 . . . . . . . 8 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (♯‘𝑥) ∈ ℕ0)
109nn0zd 11727 . . . . . . 7 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (♯‘𝑥) ∈ ℤ)
11 pgpssslw.3 . . . . . . 7 𝐹 = (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} ↦ (♯‘𝑥))
1210, 11fmptd 6574 . . . . . 6 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝐹:{𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}⟶ℤ)
1312frnd 6230 . . . . 5 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ran 𝐹 ⊆ ℤ)
14 fvex 6388 . . . . . . . 8 (♯‘𝑥) ∈ V
1514, 11fnmpti 6200 . . . . . . 7 𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}
16 simp1 1166 . . . . . . . 8 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝐻 ∈ (SubGrp‘𝐺))
17 simp3 1168 . . . . . . . 8 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝑃 pGrp 𝑆)
18 eqimss2 3818 . . . . . . . . . . 11 (𝑦 = 𝐻𝐻𝑦)
1918biantrud 527 . . . . . . . . . 10 (𝑦 = 𝐻 → (𝑃 pGrp (𝐺s 𝑦) ↔ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)))
20 oveq2 6850 . . . . . . . . . . . 12 (𝑦 = 𝐻 → (𝐺s 𝑦) = (𝐺s 𝐻))
21 pgpssslw.2 . . . . . . . . . . . 12 𝑆 = (𝐺s 𝐻)
2220, 21syl6eqr 2817 . . . . . . . . . . 11 (𝑦 = 𝐻 → (𝐺s 𝑦) = 𝑆)
2322breq2d 4821 . . . . . . . . . 10 (𝑦 = 𝐻 → (𝑃 pGrp (𝐺s 𝑦) ↔ 𝑃 pGrp 𝑆))
2419, 23bitr3d 272 . . . . . . . . 9 (𝑦 = 𝐻 → ((𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦) ↔ 𝑃 pGrp 𝑆))
2524elrab 3519 . . . . . . . 8 (𝐻 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} ↔ (𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑃 pGrp 𝑆))
2616, 17, 25sylanbrc 578 . . . . . . 7 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝐻 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)})
27 fnfvelrn 6546 . . . . . . 7 ((𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} ∧ 𝐻 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (𝐹𝐻) ∈ ran 𝐹)
2815, 26, 27sylancr 581 . . . . . 6 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (𝐹𝐻) ∈ ran 𝐹)
2928ne0d 4086 . . . . 5 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ran 𝐹 ≠ ∅)
30 hashcl 13349 . . . . . . . 8 (𝑋 ∈ Fin → (♯‘𝑋) ∈ ℕ0)
311, 30syl 17 . . . . . . 7 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (♯‘𝑋) ∈ ℕ0)
3231nn0red 11599 . . . . . 6 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (♯‘𝑋) ∈ ℝ)
33 fveq2 6375 . . . . . . . . . . 11 (𝑥 = 𝑚 → (♯‘𝑥) = (♯‘𝑚))
34 fvex 6388 . . . . . . . . . . 11 (♯‘𝑚) ∈ V
3533, 11, 34fvmpt 6471 . . . . . . . . . 10 (𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} → (𝐹𝑚) = (♯‘𝑚))
3635adantl 473 . . . . . . . . 9 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (𝐹𝑚) = (♯‘𝑚))
37 oveq2 6850 . . . . . . . . . . . . 13 (𝑦 = 𝑚 → (𝐺s 𝑦) = (𝐺s 𝑚))
3837breq2d 4821 . . . . . . . . . . . 12 (𝑦 = 𝑚 → (𝑃 pGrp (𝐺s 𝑦) ↔ 𝑃 pGrp (𝐺s 𝑚)))
39 sseq2 3787 . . . . . . . . . . . 12 (𝑦 = 𝑚 → (𝐻𝑦𝐻𝑚))
4038, 39anbi12d 624 . . . . . . . . . . 11 (𝑦 = 𝑚 → ((𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦) ↔ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚)))
4140elrab 3519 . . . . . . . . . 10 (𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} ↔ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚)))
421adantr 472 . . . . . . . . . . . 12 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))) → 𝑋 ∈ Fin)
433subgss 17861 . . . . . . . . . . . . 13 (𝑚 ∈ (SubGrp‘𝐺) → 𝑚𝑋)
4443ad2antrl 719 . . . . . . . . . . . 12 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))) → 𝑚𝑋)
45 ssdomg 8206 . . . . . . . . . . . 12 (𝑋 ∈ Fin → (𝑚𝑋𝑚𝑋))
4642, 44, 45sylc 65 . . . . . . . . . . 11 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))) → 𝑚𝑋)
47 ssfi 8387 . . . . . . . . . . . . 13 ((𝑋 ∈ Fin ∧ 𝑚𝑋) → 𝑚 ∈ Fin)
4842, 44, 47syl2anc 579 . . . . . . . . . . . 12 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))) → 𝑚 ∈ Fin)
49 hashdom 13370 . . . . . . . . . . . 12 ((𝑚 ∈ Fin ∧ 𝑋 ∈ Fin) → ((♯‘𝑚) ≤ (♯‘𝑋) ↔ 𝑚𝑋))
5048, 42, 49syl2anc 579 . . . . . . . . . . 11 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))) → ((♯‘𝑚) ≤ (♯‘𝑋) ↔ 𝑚𝑋))
5146, 50mpbird 248 . . . . . . . . . 10 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))) → (♯‘𝑚) ≤ (♯‘𝑋))
5241, 51sylan2b 587 . . . . . . . . 9 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (♯‘𝑚) ≤ (♯‘𝑋))
5336, 52eqbrtrd 4831 . . . . . . . 8 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (𝐹𝑚) ≤ (♯‘𝑋))
5453ralrimiva 3113 . . . . . . 7 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∀𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑚) ≤ (♯‘𝑋))
55 breq1 4812 . . . . . . . . 9 (𝑤 = (𝐹𝑚) → (𝑤 ≤ (♯‘𝑋) ↔ (𝐹𝑚) ≤ (♯‘𝑋)))
5655ralrn 6552 . . . . . . . 8 (𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} → (∀𝑤 ∈ ran 𝐹 𝑤 ≤ (♯‘𝑋) ↔ ∀𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑚) ≤ (♯‘𝑋)))
5715, 56ax-mp 5 . . . . . . 7 (∀𝑤 ∈ ran 𝐹 𝑤 ≤ (♯‘𝑋) ↔ ∀𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑚) ≤ (♯‘𝑋))
5854, 57sylibr 225 . . . . . 6 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∀𝑤 ∈ ran 𝐹 𝑤 ≤ (♯‘𝑋))
59 brralrspcev 4869 . . . . . 6 (((♯‘𝑋) ∈ ℝ ∧ ∀𝑤 ∈ ran 𝐹 𝑤 ≤ (♯‘𝑋)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤𝑧)
6032, 58, 59syl2anc 579 . . . . 5 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤𝑧)
61 suprzcl 11704 . . . . 5 ((ran 𝐹 ⊆ ℤ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤𝑧) → sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹)
6213, 29, 60, 61syl3anc 1490 . . . 4 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹)
63 fvelrnb 6432 . . . . 5 (𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} → (sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ↔ ∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))
6415, 63ax-mp 5 . . . 4 (sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ↔ ∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑘) = sup(ran 𝐹, ℝ, < ))
6562, 64sylib 209 . . 3 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑘) = sup(ran 𝐹, ℝ, < ))
66 oveq2 6850 . . . . . 6 (𝑦 = 𝑘 → (𝐺s 𝑦) = (𝐺s 𝑘))
6766breq2d 4821 . . . . 5 (𝑦 = 𝑘 → (𝑃 pGrp (𝐺s 𝑦) ↔ 𝑃 pGrp (𝐺s 𝑘)))
68 sseq2 3787 . . . . 5 (𝑦 = 𝑘 → (𝐻𝑦𝐻𝑘))
6967, 68anbi12d 624 . . . 4 (𝑦 = 𝑘 → ((𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦) ↔ (𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘)))
7069rexrab 3527 . . 3 (∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} (𝐹𝑘) = sup(ran 𝐹, ℝ, < ) ↔ ∃𝑘 ∈ (SubGrp‘𝐺)((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))
7165, 70sylib 209 . 2 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ (SubGrp‘𝐺)((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))
72 simpl3 1246 . . . 4 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑃 pGrp 𝑆)
73 pgpprm 18274 . . . 4 (𝑃 pGrp 𝑆𝑃 ∈ ℙ)
7472, 73syl 17 . . 3 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑃 ∈ ℙ)
75 simprl 787 . . 3 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑘 ∈ (SubGrp‘𝐺))
76 zssre 11631 . . . . . . . . . . . . 13 ℤ ⊆ ℝ
7713, 76syl6ss 3773 . . . . . . . . . . . 12 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ran 𝐹 ⊆ ℝ)
7877ad2antrr 717 . . . . . . . . . . 11 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ran 𝐹 ⊆ ℝ)
7929ad2antrr 717 . . . . . . . . . . 11 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ran 𝐹 ≠ ∅)
8060ad2antrr 717 . . . . . . . . . . 11 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤𝑧)
81 simprl 787 . . . . . . . . . . . . . 14 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑚 ∈ (SubGrp‘𝐺))
82 simprrr 800 . . . . . . . . . . . . . . 15 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑃 pGrp (𝐺s 𝑚))
83 simprrl 799 . . . . . . . . . . . . . . . . . 18 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → (𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘))
8483adantr 472 . . . . . . . . . . . . . . . . 17 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘))
8584simprd 489 . . . . . . . . . . . . . . . 16 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝐻𝑘)
86 simprrl 799 . . . . . . . . . . . . . . . 16 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑘𝑚)
8785, 86sstrd 3771 . . . . . . . . . . . . . . 15 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝐻𝑚)
8882, 87jca 507 . . . . . . . . . . . . . 14 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝑃 pGrp (𝐺s 𝑚) ∧ 𝐻𝑚))
8981, 88, 41sylanbrc 578 . . . . . . . . . . . . 13 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)})
9089, 35syl 17 . . . . . . . . . . . 12 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝐹𝑚) = (♯‘𝑚))
91 fnfvelrn 6546 . . . . . . . . . . . . 13 ((𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)}) → (𝐹𝑚) ∈ ran 𝐹)
9215, 89, 91sylancr 581 . . . . . . . . . . . 12 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝐹𝑚) ∈ ran 𝐹)
9390, 92eqeltrrd 2845 . . . . . . . . . . 11 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (♯‘𝑚) ∈ ran 𝐹)
94 suprub 11238 . . . . . . . . . . 11 (((ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤𝑧) ∧ (♯‘𝑚) ∈ ran 𝐹) → (♯‘𝑚) ≤ sup(ran 𝐹, ℝ, < ))
9578, 79, 80, 93, 94syl31anc 1492 . . . . . . . . . 10 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (♯‘𝑚) ≤ sup(ran 𝐹, ℝ, < ))
96 simprrr 800 . . . . . . . . . . . 12 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → (𝐹𝑘) = sup(ran 𝐹, ℝ, < ))
9796adantr 472 . . . . . . . . . . 11 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝐹𝑘) = sup(ran 𝐹, ℝ, < ))
9875adantr 472 . . . . . . . . . . . . 13 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑘 ∈ (SubGrp‘𝐺))
9969elrab 3519 . . . . . . . . . . . . 13 (𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} ↔ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘)))
10098, 84, 99sylanbrc 578 . . . . . . . . . . . 12 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)})
101 fveq2 6375 . . . . . . . . . . . . 13 (𝑥 = 𝑘 → (♯‘𝑥) = (♯‘𝑘))
102 fvex 6388 . . . . . . . . . . . . 13 (♯‘𝑘) ∈ V
103101, 11, 102fvmpt 6471 . . . . . . . . . . . 12 (𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺s 𝑦) ∧ 𝐻𝑦)} → (𝐹𝑘) = (♯‘𝑘))
104100, 103syl 17 . . . . . . . . . . 11 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝐹𝑘) = (♯‘𝑘))
10597, 104eqtr3d 2801 . . . . . . . . . 10 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → sup(ran 𝐹, ℝ, < ) = (♯‘𝑘))
10695, 105breqtrd 4835 . . . . . . . . 9 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (♯‘𝑚) ≤ (♯‘𝑘))
107 simpll2 1271 . . . . . . . . . . 11 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑋 ∈ Fin)
10843ad2antrl 719 . . . . . . . . . . 11 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑚𝑋)
109107, 108, 47syl2anc 579 . . . . . . . . . 10 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑚 ∈ Fin)
110 ssfi 8387 . . . . . . . . . . 11 ((𝑚 ∈ Fin ∧ 𝑘𝑚) → 𝑘 ∈ Fin)
111109, 86, 110syl2anc 579 . . . . . . . . . 10 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑘 ∈ Fin)
112 hashcl 13349 . . . . . . . . . . 11 (𝑚 ∈ Fin → (♯‘𝑚) ∈ ℕ0)
113 hashcl 13349 . . . . . . . . . . 11 (𝑘 ∈ Fin → (♯‘𝑘) ∈ ℕ0)
114 nn0re 11548 . . . . . . . . . . . 12 ((♯‘𝑚) ∈ ℕ0 → (♯‘𝑚) ∈ ℝ)
115 nn0re 11548 . . . . . . . . . . . 12 ((♯‘𝑘) ∈ ℕ0 → (♯‘𝑘) ∈ ℝ)
116 lenlt 10370 . . . . . . . . . . . 12 (((♯‘𝑚) ∈ ℝ ∧ (♯‘𝑘) ∈ ℝ) → ((♯‘𝑚) ≤ (♯‘𝑘) ↔ ¬ (♯‘𝑘) < (♯‘𝑚)))
117114, 115, 116syl2an 589 . . . . . . . . . . 11 (((♯‘𝑚) ∈ ℕ0 ∧ (♯‘𝑘) ∈ ℕ0) → ((♯‘𝑚) ≤ (♯‘𝑘) ↔ ¬ (♯‘𝑘) < (♯‘𝑚)))
118112, 113, 117syl2an 589 . . . . . . . . . 10 ((𝑚 ∈ Fin ∧ 𝑘 ∈ Fin) → ((♯‘𝑚) ≤ (♯‘𝑘) ↔ ¬ (♯‘𝑘) < (♯‘𝑚)))
119109, 111, 118syl2anc 579 . . . . . . . . 9 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ((♯‘𝑚) ≤ (♯‘𝑘) ↔ ¬ (♯‘𝑘) < (♯‘𝑚)))
120106, 119mpbid 223 . . . . . . . 8 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ¬ (♯‘𝑘) < (♯‘𝑚))
121 php3 8353 . . . . . . . . . . 11 ((𝑚 ∈ Fin ∧ 𝑘𝑚) → 𝑘𝑚)
122121ex 401 . . . . . . . . . 10 (𝑚 ∈ Fin → (𝑘𝑚𝑘𝑚))
123109, 122syl 17 . . . . . . . . 9 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝑘𝑚𝑘𝑚))
124 hashsdom 13372 . . . . . . . . . 10 ((𝑘 ∈ Fin ∧ 𝑚 ∈ Fin) → ((♯‘𝑘) < (♯‘𝑚) ↔ 𝑘𝑚))
125111, 109, 124syl2anc 579 . . . . . . . . 9 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ((♯‘𝑘) < (♯‘𝑚) ↔ 𝑘𝑚))
126123, 125sylibrd 250 . . . . . . . 8 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝑘𝑚 → (♯‘𝑘) < (♯‘𝑚)))
127120, 126mtod 189 . . . . . . 7 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → ¬ 𝑘𝑚)
128 sspss 3867 . . . . . . . . 9 (𝑘𝑚 ↔ (𝑘𝑚𝑘 = 𝑚))
12986, 128sylib 209 . . . . . . . 8 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (𝑘𝑚𝑘 = 𝑚))
130129ord 890 . . . . . . 7 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → (¬ 𝑘𝑚𝑘 = 𝑚))
131127, 130mpd 15 . . . . . 6 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚)))) → 𝑘 = 𝑚)
132131expr 448 . . . . 5 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → ((𝑘𝑚𝑃 pGrp (𝐺s 𝑚)) → 𝑘 = 𝑚))
13383simpld 488 . . . . . . 7 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑃 pGrp (𝐺s 𝑘))
134133adantr 472 . . . . . 6 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺s 𝑘))
135 oveq2 6850 . . . . . . . 8 (𝑘 = 𝑚 → (𝐺s 𝑘) = (𝐺s 𝑚))
136135breq2d 4821 . . . . . . 7 (𝑘 = 𝑚 → (𝑃 pGrp (𝐺s 𝑘) ↔ 𝑃 pGrp (𝐺s 𝑚)))
137 eqimss 3817 . . . . . . . 8 (𝑘 = 𝑚𝑘𝑚)
138137biantrurd 528 . . . . . . 7 (𝑘 = 𝑚 → (𝑃 pGrp (𝐺s 𝑚) ↔ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚))))
139136, 138bitrd 270 . . . . . 6 (𝑘 = 𝑚 → (𝑃 pGrp (𝐺s 𝑘) ↔ (𝑘𝑚𝑃 pGrp (𝐺s 𝑚))))
140134, 139syl5ibcom 236 . . . . 5 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → (𝑘 = 𝑚 → (𝑘𝑚𝑃 pGrp (𝐺s 𝑚))))
141132, 140impbid 203 . . . 4 ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → ((𝑘𝑚𝑃 pGrp (𝐺s 𝑚)) ↔ 𝑘 = 𝑚))
142141ralrimiva 3113 . . 3 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → ∀𝑚 ∈ (SubGrp‘𝐺)((𝑘𝑚𝑃 pGrp (𝐺s 𝑚)) ↔ 𝑘 = 𝑚))
143 isslw 18289 . . 3 (𝑘 ∈ (𝑃 pSyl 𝐺) ↔ (𝑃 ∈ ℙ ∧ 𝑘 ∈ (SubGrp‘𝐺) ∧ ∀𝑚 ∈ (SubGrp‘𝐺)((𝑘𝑚𝑃 pGrp (𝐺s 𝑚)) ↔ 𝑘 = 𝑚)))
14474, 75, 142, 143syl3anbrc 1443 . 2 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑘 ∈ (𝑃 pSyl 𝐺))
14583simprd 489 . 2 (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺s 𝑘) ∧ 𝐻𝑘) ∧ (𝐹𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝐻𝑘)
14671, 144, 145reximssdv 3165 1 ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ (𝑃 pSyl 𝐺)𝐻𝑘)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  wss 3732  wpss 3733  c0 4079   class class class wbr 4809  cmpt 4888  ran crn 5278   Fn wfn 6063  cfv 6068  (class class class)co 6842  cdom 8158  csdm 8159  Fincfn 8160  supcsup 8553  cr 10188   < clt 10328  cle 10329  0cn0 11538  cz 11624  chash 13321  cprime 15667  Basecbs 16132  s cress 16133  SubGrpcsubg 17854   pGrp cpgp 18212   pSyl cslw 18213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-sup 8555  df-card 9016  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-n0 11539  df-xnn0 11611  df-z 11625  df-uz 11887  df-fz 12534  df-hash 13322  df-subg 17857  df-pgp 18216  df-slw 18217
This theorem is referenced by:  slwn0  18296
  Copyright terms: Public domain W3C validator