| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp2 1138 | . . . . . . . . . 10
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝑋 ∈ Fin) | 
| 2 |  | elrabi 3687 | . . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} → 𝑥 ∈ (SubGrp‘𝐺)) | 
| 3 |  | pgpssslw.1 | . . . . . . . . . . . 12
⊢ 𝑋 = (Base‘𝐺) | 
| 4 | 3 | subgss 19145 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (SubGrp‘𝐺) → 𝑥 ⊆ 𝑋) | 
| 5 | 2, 4 | syl 17 | . . . . . . . . . 10
⊢ (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} → 𝑥 ⊆ 𝑋) | 
| 6 |  | ssfi 9213 | . . . . . . . . . 10
⊢ ((𝑋 ∈ Fin ∧ 𝑥 ⊆ 𝑋) → 𝑥 ∈ Fin) | 
| 7 | 1, 5, 6 | syl2an 596 | . . . . . . . . 9
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → 𝑥 ∈ Fin) | 
| 8 |  | hashcl 14395 | . . . . . . . . 9
⊢ (𝑥 ∈ Fin →
(♯‘𝑥) ∈
ℕ0) | 
| 9 | 7, 8 | syl 17 | . . . . . . . 8
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (♯‘𝑥) ∈
ℕ0) | 
| 10 | 9 | nn0zd 12639 | . . . . . . 7
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (♯‘𝑥) ∈ ℤ) | 
| 11 |  | pgpssslw.3 | . . . . . . 7
⊢ 𝐹 = (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} ↦ (♯‘𝑥)) | 
| 12 | 10, 11 | fmptd 7134 | . . . . . 6
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝐹:{𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}⟶ℤ) | 
| 13 | 12 | frnd 6744 | . . . . 5
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ran 𝐹 ⊆ ℤ) | 
| 14 |  | fvex 6919 | . . . . . . . 8
⊢
(♯‘𝑥)
∈ V | 
| 15 | 14, 11 | fnmpti 6711 | . . . . . . 7
⊢ 𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} | 
| 16 |  | eqimss2 4043 | . . . . . . . . . 10
⊢ (𝑦 = 𝐻 → 𝐻 ⊆ 𝑦) | 
| 17 | 16 | biantrud 531 | . . . . . . . . 9
⊢ (𝑦 = 𝐻 → (𝑃 pGrp (𝐺 ↾s 𝑦) ↔ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦))) | 
| 18 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑦 = 𝐻 → (𝐺 ↾s 𝑦) = (𝐺 ↾s 𝐻)) | 
| 19 |  | pgpssslw.2 | . . . . . . . . . . 11
⊢ 𝑆 = (𝐺 ↾s 𝐻) | 
| 20 | 18, 19 | eqtr4di 2795 | . . . . . . . . . 10
⊢ (𝑦 = 𝐻 → (𝐺 ↾s 𝑦) = 𝑆) | 
| 21 | 20 | breq2d 5155 | . . . . . . . . 9
⊢ (𝑦 = 𝐻 → (𝑃 pGrp (𝐺 ↾s 𝑦) ↔ 𝑃 pGrp 𝑆)) | 
| 22 | 17, 21 | bitr3d 281 | . . . . . . . 8
⊢ (𝑦 = 𝐻 → ((𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦) ↔ 𝑃 pGrp 𝑆)) | 
| 23 |  | simp1 1137 | . . . . . . . 8
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝐻 ∈ (SubGrp‘𝐺)) | 
| 24 |  | simp3 1139 | . . . . . . . 8
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝑃 pGrp 𝑆) | 
| 25 | 22, 23, 24 | elrabd 3694 | . . . . . . 7
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝐻 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) | 
| 26 |  | fnfvelrn 7100 | . . . . . . 7
⊢ ((𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} ∧ 𝐻 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (𝐹‘𝐻) ∈ ran 𝐹) | 
| 27 | 15, 25, 26 | sylancr 587 | . . . . . 6
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (𝐹‘𝐻) ∈ ran 𝐹) | 
| 28 | 27 | ne0d 4342 | . . . . 5
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ran 𝐹 ≠ ∅) | 
| 29 |  | hashcl 14395 | . . . . . . . 8
⊢ (𝑋 ∈ Fin →
(♯‘𝑋) ∈
ℕ0) | 
| 30 | 1, 29 | syl 17 | . . . . . . 7
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (♯‘𝑋) ∈
ℕ0) | 
| 31 | 30 | nn0red 12588 | . . . . . 6
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (♯‘𝑋) ∈ ℝ) | 
| 32 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑚 → (♯‘𝑥) = (♯‘𝑚)) | 
| 33 |  | fvex 6919 | . . . . . . . . . . 11
⊢
(♯‘𝑚)
∈ V | 
| 34 | 32, 11, 33 | fvmpt 7016 | . . . . . . . . . 10
⊢ (𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} → (𝐹‘𝑚) = (♯‘𝑚)) | 
| 35 | 34 | adantl 481 | . . . . . . . . 9
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (𝐹‘𝑚) = (♯‘𝑚)) | 
| 36 |  | oveq2 7439 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑚 → (𝐺 ↾s 𝑦) = (𝐺 ↾s 𝑚)) | 
| 37 | 36 | breq2d 5155 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑚 → (𝑃 pGrp (𝐺 ↾s 𝑦) ↔ 𝑃 pGrp (𝐺 ↾s 𝑚))) | 
| 38 |  | sseq2 4010 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑚 → (𝐻 ⊆ 𝑦 ↔ 𝐻 ⊆ 𝑚)) | 
| 39 | 37, 38 | anbi12d 632 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑚 → ((𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦) ↔ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) | 
| 40 | 39 | elrab 3692 | . . . . . . . . . 10
⊢ (𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} ↔ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) | 
| 41 | 1 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) → 𝑋 ∈ Fin) | 
| 42 | 3 | subgss 19145 | . . . . . . . . . . . . 13
⊢ (𝑚 ∈ (SubGrp‘𝐺) → 𝑚 ⊆ 𝑋) | 
| 43 | 42 | ad2antrl 728 | . . . . . . . . . . . 12
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) → 𝑚 ⊆ 𝑋) | 
| 44 |  | ssdomg 9040 | . . . . . . . . . . . 12
⊢ (𝑋 ∈ Fin → (𝑚 ⊆ 𝑋 → 𝑚 ≼ 𝑋)) | 
| 45 | 41, 43, 44 | sylc 65 | . . . . . . . . . . 11
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) → 𝑚 ≼ 𝑋) | 
| 46 | 41, 43 | ssfid 9301 | . . . . . . . . . . . 12
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) → 𝑚 ∈ Fin) | 
| 47 |  | hashdom 14418 | . . . . . . . . . . . 12
⊢ ((𝑚 ∈ Fin ∧ 𝑋 ∈ Fin) →
((♯‘𝑚) ≤
(♯‘𝑋) ↔
𝑚 ≼ 𝑋)) | 
| 48 | 46, 41, 47 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) → ((♯‘𝑚) ≤ (♯‘𝑋) ↔ 𝑚 ≼ 𝑋)) | 
| 49 | 45, 48 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) → (♯‘𝑚) ≤ (♯‘𝑋)) | 
| 50 | 40, 49 | sylan2b 594 | . . . . . . . . 9
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (♯‘𝑚) ≤ (♯‘𝑋)) | 
| 51 | 35, 50 | eqbrtrd 5165 | . . . . . . . 8
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (𝐹‘𝑚) ≤ (♯‘𝑋)) | 
| 52 | 51 | ralrimiva 3146 | . . . . . . 7
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∀𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑚) ≤ (♯‘𝑋)) | 
| 53 |  | breq1 5146 | . . . . . . . . 9
⊢ (𝑤 = (𝐹‘𝑚) → (𝑤 ≤ (♯‘𝑋) ↔ (𝐹‘𝑚) ≤ (♯‘𝑋))) | 
| 54 | 53 | ralrn 7108 | . . . . . . . 8
⊢ (𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} → (∀𝑤 ∈ ran 𝐹 𝑤 ≤ (♯‘𝑋) ↔ ∀𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑚) ≤ (♯‘𝑋))) | 
| 55 | 15, 54 | ax-mp 5 | . . . . . . 7
⊢
(∀𝑤 ∈
ran 𝐹 𝑤 ≤ (♯‘𝑋) ↔ ∀𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑚) ≤ (♯‘𝑋)) | 
| 56 | 52, 55 | sylibr 234 | . . . . . 6
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∀𝑤 ∈ ran 𝐹 𝑤 ≤ (♯‘𝑋)) | 
| 57 |  | brralrspcev 5203 | . . . . . 6
⊢
(((♯‘𝑋)
∈ ℝ ∧ ∀𝑤 ∈ ran 𝐹 𝑤 ≤ (♯‘𝑋)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧) | 
| 58 | 31, 56, 57 | syl2anc 584 | . . . . 5
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧) | 
| 59 |  | suprzcl 12698 | . . . . 5
⊢ ((ran
𝐹 ⊆ ℤ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑧 ∈ ℝ
∀𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧) → sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹) | 
| 60 | 13, 28, 58, 59 | syl3anc 1373 | . . . 4
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹) | 
| 61 |  | fvelrnb 6969 | . . . . 5
⊢ (𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} → (sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ↔ ∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < ))) | 
| 62 | 15, 61 | ax-mp 5 | . . . 4
⊢ (sup(ran
𝐹, ℝ, < ) ∈
ran 𝐹 ↔ ∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )) | 
| 63 | 60, 62 | sylib 218 | . . 3
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )) | 
| 64 |  | oveq2 7439 | . . . . . 6
⊢ (𝑦 = 𝑘 → (𝐺 ↾s 𝑦) = (𝐺 ↾s 𝑘)) | 
| 65 | 64 | breq2d 5155 | . . . . 5
⊢ (𝑦 = 𝑘 → (𝑃 pGrp (𝐺 ↾s 𝑦) ↔ 𝑃 pGrp (𝐺 ↾s 𝑘))) | 
| 66 |  | sseq2 4010 | . . . . 5
⊢ (𝑦 = 𝑘 → (𝐻 ⊆ 𝑦 ↔ 𝐻 ⊆ 𝑘)) | 
| 67 | 65, 66 | anbi12d 632 | . . . 4
⊢ (𝑦 = 𝑘 → ((𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦) ↔ (𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘))) | 
| 68 | 67 | rexrab 3702 | . . 3
⊢
(∃𝑘 ∈
{𝑦 ∈
(SubGrp‘𝐺) ∣
(𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < ) ↔ ∃𝑘 ∈ (SubGrp‘𝐺)((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < ))) | 
| 69 | 63, 68 | sylib 218 | . 2
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ (SubGrp‘𝐺)((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < ))) | 
| 70 |  | simpl3 1194 | . . . 4
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑃 pGrp 𝑆) | 
| 71 |  | pgpprm 19611 | . . . 4
⊢ (𝑃 pGrp 𝑆 → 𝑃 ∈ ℙ) | 
| 72 | 70, 71 | syl 17 | . . 3
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑃 ∈
ℙ) | 
| 73 |  | simprl 771 | . . 3
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑘 ∈ (SubGrp‘𝐺)) | 
| 74 |  | zssre 12620 | . . . . . . . . . . . . 13
⊢ ℤ
⊆ ℝ | 
| 75 | 13, 74 | sstrdi 3996 | . . . . . . . . . . . 12
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ran 𝐹 ⊆ ℝ) | 
| 76 | 75 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ran 𝐹 ⊆ ℝ) | 
| 77 | 28 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ran 𝐹 ≠ ∅) | 
| 78 | 58 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧) | 
| 79 |  | simprl 771 | . . . . . . . . . . . . . 14
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑚 ∈ (SubGrp‘𝐺)) | 
| 80 |  | simprrr 782 | . . . . . . . . . . . . . . 15
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑃 pGrp (𝐺 ↾s 𝑚)) | 
| 81 |  | simprrl 781 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → (𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘)) | 
| 82 | 81 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘)) | 
| 83 | 82 | simprd 495 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝐻 ⊆ 𝑘) | 
| 84 |  | simprrl 781 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑘 ⊆ 𝑚) | 
| 85 | 83, 84 | sstrd 3994 | . . . . . . . . . . . . . . 15
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝐻 ⊆ 𝑚) | 
| 86 | 80, 85 | jca 511 | . . . . . . . . . . . . . 14
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚)) | 
| 87 | 39, 79, 86 | elrabd 3694 | . . . . . . . . . . . . 13
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) | 
| 88 | 87, 34 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝐹‘𝑚) = (♯‘𝑚)) | 
| 89 |  | fnfvelrn 7100 | . . . . . . . . . . . . 13
⊢ ((𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (𝐹‘𝑚) ∈ ran 𝐹) | 
| 90 | 15, 87, 89 | sylancr 587 | . . . . . . . . . . . 12
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝐹‘𝑚) ∈ ran 𝐹) | 
| 91 | 88, 90 | eqeltrrd 2842 | . . . . . . . . . . 11
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (♯‘𝑚) ∈ ran 𝐹) | 
| 92 | 76, 77, 78, 91 | suprubd 12230 | . . . . . . . . . 10
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (♯‘𝑚) ≤ sup(ran 𝐹, ℝ, < )) | 
| 93 |  | simprrr 782 | . . . . . . . . . . . 12
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )) | 
| 94 | 93 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )) | 
| 95 | 73 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑘 ∈ (SubGrp‘𝐺)) | 
| 96 | 67, 95, 82 | elrabd 3694 | . . . . . . . . . . . 12
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) | 
| 97 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑘 → (♯‘𝑥) = (♯‘𝑘)) | 
| 98 |  | fvex 6919 | . . . . . . . . . . . . 13
⊢
(♯‘𝑘)
∈ V | 
| 99 | 97, 11, 98 | fvmpt 7016 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} → (𝐹‘𝑘) = (♯‘𝑘)) | 
| 100 | 96, 99 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝐹‘𝑘) = (♯‘𝑘)) | 
| 101 | 94, 100 | eqtr3d 2779 | . . . . . . . . . 10
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → sup(ran 𝐹, ℝ, < ) = (♯‘𝑘)) | 
| 102 | 92, 101 | breqtrd 5169 | . . . . . . . . 9
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (♯‘𝑚) ≤ (♯‘𝑘)) | 
| 103 |  | simpll2 1214 | . . . . . . . . . . 11
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑋 ∈ Fin) | 
| 104 | 42 | ad2antrl 728 | . . . . . . . . . . 11
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑚 ⊆ 𝑋) | 
| 105 | 103, 104 | ssfid 9301 | . . . . . . . . . 10
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑚 ∈ Fin) | 
| 106 | 105, 84 | ssfid 9301 | . . . . . . . . . 10
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑘 ∈ Fin) | 
| 107 |  | hashcl 14395 | . . . . . . . . . . 11
⊢ (𝑚 ∈ Fin →
(♯‘𝑚) ∈
ℕ0) | 
| 108 |  | hashcl 14395 | . . . . . . . . . . 11
⊢ (𝑘 ∈ Fin →
(♯‘𝑘) ∈
ℕ0) | 
| 109 |  | nn0re 12535 | . . . . . . . . . . . 12
⊢
((♯‘𝑚)
∈ ℕ0 → (♯‘𝑚) ∈ ℝ) | 
| 110 |  | nn0re 12535 | . . . . . . . . . . . 12
⊢
((♯‘𝑘)
∈ ℕ0 → (♯‘𝑘) ∈ ℝ) | 
| 111 |  | lenlt 11339 | . . . . . . . . . . . 12
⊢
(((♯‘𝑚)
∈ ℝ ∧ (♯‘𝑘) ∈ ℝ) →
((♯‘𝑚) ≤
(♯‘𝑘) ↔
¬ (♯‘𝑘)
< (♯‘𝑚))) | 
| 112 | 109, 110,
111 | syl2an 596 | . . . . . . . . . . 11
⊢
(((♯‘𝑚)
∈ ℕ0 ∧ (♯‘𝑘) ∈ ℕ0) →
((♯‘𝑚) ≤
(♯‘𝑘) ↔
¬ (♯‘𝑘)
< (♯‘𝑚))) | 
| 113 | 107, 108,
112 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝑚 ∈ Fin ∧ 𝑘 ∈ Fin) →
((♯‘𝑚) ≤
(♯‘𝑘) ↔
¬ (♯‘𝑘)
< (♯‘𝑚))) | 
| 114 | 105, 106,
113 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ((♯‘𝑚) ≤ (♯‘𝑘) ↔ ¬
(♯‘𝑘) <
(♯‘𝑚))) | 
| 115 | 102, 114 | mpbid 232 | . . . . . . . 8
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ¬ (♯‘𝑘) < (♯‘𝑚)) | 
| 116 |  | php3 9249 | . . . . . . . . . . 11
⊢ ((𝑚 ∈ Fin ∧ 𝑘 ⊊ 𝑚) → 𝑘 ≺ 𝑚) | 
| 117 | 116 | ex 412 | . . . . . . . . . 10
⊢ (𝑚 ∈ Fin → (𝑘 ⊊ 𝑚 → 𝑘 ≺ 𝑚)) | 
| 118 | 105, 117 | syl 17 | . . . . . . . . 9
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝑘 ⊊ 𝑚 → 𝑘 ≺ 𝑚)) | 
| 119 |  | hashsdom 14420 | . . . . . . . . . 10
⊢ ((𝑘 ∈ Fin ∧ 𝑚 ∈ Fin) →
((♯‘𝑘) <
(♯‘𝑚) ↔
𝑘 ≺ 𝑚)) | 
| 120 | 106, 105,
119 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ((♯‘𝑘) < (♯‘𝑚) ↔ 𝑘 ≺ 𝑚)) | 
| 121 | 118, 120 | sylibrd 259 | . . . . . . . 8
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝑘 ⊊ 𝑚 → (♯‘𝑘) < (♯‘𝑚))) | 
| 122 | 115, 121 | mtod 198 | . . . . . . 7
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ¬ 𝑘 ⊊ 𝑚) | 
| 123 |  | sspss 4102 | . . . . . . . . 9
⊢ (𝑘 ⊆ 𝑚 ↔ (𝑘 ⊊ 𝑚 ∨ 𝑘 = 𝑚)) | 
| 124 | 84, 123 | sylib 218 | . . . . . . . 8
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝑘 ⊊ 𝑚 ∨ 𝑘 = 𝑚)) | 
| 125 | 124 | ord 865 | . . . . . . 7
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (¬ 𝑘 ⊊ 𝑚 → 𝑘 = 𝑚)) | 
| 126 | 122, 125 | mpd 15 | . . . . . 6
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑘 = 𝑚) | 
| 127 | 126 | expr 456 | . . . . 5
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → ((𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)) → 𝑘 = 𝑚)) | 
| 128 | 81 | simpld 494 | . . . . . . 7
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑃 pGrp (𝐺 ↾s 𝑘)) | 
| 129 | 128 | adantr 480 | . . . . . 6
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾s 𝑘)) | 
| 130 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑘 = 𝑚 → (𝐺 ↾s 𝑘) = (𝐺 ↾s 𝑚)) | 
| 131 | 130 | breq2d 5155 | . . . . . . 7
⊢ (𝑘 = 𝑚 → (𝑃 pGrp (𝐺 ↾s 𝑘) ↔ 𝑃 pGrp (𝐺 ↾s 𝑚))) | 
| 132 |  | eqimss 4042 | . . . . . . . 8
⊢ (𝑘 = 𝑚 → 𝑘 ⊆ 𝑚) | 
| 133 | 132 | biantrurd 532 | . . . . . . 7
⊢ (𝑘 = 𝑚 → (𝑃 pGrp (𝐺 ↾s 𝑚) ↔ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) | 
| 134 | 131, 133 | bitrd 279 | . . . . . 6
⊢ (𝑘 = 𝑚 → (𝑃 pGrp (𝐺 ↾s 𝑘) ↔ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) | 
| 135 | 129, 134 | syl5ibcom 245 | . . . . 5
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → (𝑘 = 𝑚 → (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) | 
| 136 | 127, 135 | impbid 212 | . . . 4
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → ((𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)) ↔ 𝑘 = 𝑚)) | 
| 137 | 136 | ralrimiva 3146 | . . 3
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → ∀𝑚 ∈ (SubGrp‘𝐺)((𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)) ↔ 𝑘 = 𝑚)) | 
| 138 |  | isslw 19626 | . . 3
⊢ (𝑘 ∈ (𝑃 pSyl 𝐺) ↔ (𝑃 ∈ ℙ ∧ 𝑘 ∈ (SubGrp‘𝐺) ∧ ∀𝑚 ∈ (SubGrp‘𝐺)((𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)) ↔ 𝑘 = 𝑚))) | 
| 139 | 72, 73, 137, 138 | syl3anbrc 1344 | . 2
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑘 ∈ (𝑃 pSyl 𝐺)) | 
| 140 | 81 | simprd 495 | . 2
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝐻 ⊆ 𝑘) | 
| 141 | 69, 139, 140 | reximssdv 3173 | 1
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ (𝑃 pSyl 𝐺)𝐻 ⊆ 𝑘) |