Step | Hyp | Ref
| Expression |
1 | | simp2 1055 |
. . . . . . . . . 10
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝑋 ∈ Fin) |
2 | | elrabi 3328 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} → 𝑥 ∈ (SubGrp‘𝐺)) |
3 | | pgpssslw.1 |
. . . . . . . . . . . 12
⊢ 𝑋 = (Base‘𝐺) |
4 | 3 | subgss 17418 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (SubGrp‘𝐺) → 𝑥 ⊆ 𝑋) |
5 | 2, 4 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} → 𝑥 ⊆ 𝑋) |
6 | | ssfi 8065 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Fin ∧ 𝑥 ⊆ 𝑋) → 𝑥 ∈ Fin) |
7 | 1, 5, 6 | syl2an 493 |
. . . . . . . . 9
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → 𝑥 ∈ Fin) |
8 | | hashcl 13009 |
. . . . . . . . 9
⊢ (𝑥 ∈ Fin →
(#‘𝑥) ∈
ℕ0) |
9 | 7, 8 | syl 17 |
. . . . . . . 8
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (#‘𝑥) ∈
ℕ0) |
10 | 9 | nn0zd 11356 |
. . . . . . 7
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (#‘𝑥) ∈ ℤ) |
11 | | pgpssslw.3 |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} ↦ (#‘𝑥)) |
12 | 10, 11 | fmptd 6292 |
. . . . . 6
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝐹:{𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}⟶ℤ) |
13 | | frn 5966 |
. . . . . 6
⊢ (𝐹:{𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}⟶ℤ → ran 𝐹 ⊆
ℤ) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ran 𝐹 ⊆ ℤ) |
15 | | fvex 6113 |
. . . . . . . 8
⊢
(#‘𝑥) ∈
V |
16 | 15, 11 | fnmpti 5935 |
. . . . . . 7
⊢ 𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} |
17 | | simp1 1054 |
. . . . . . . 8
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝐻 ∈ (SubGrp‘𝐺)) |
18 | | simp3 1056 |
. . . . . . . 8
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝑃 pGrp 𝑆) |
19 | | eqimss2 3621 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐻 → 𝐻 ⊆ 𝑦) |
20 | 19 | biantrud 527 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐻 → (𝑃 pGrp (𝐺 ↾s 𝑦) ↔ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦))) |
21 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐻 → (𝐺 ↾s 𝑦) = (𝐺 ↾s 𝐻)) |
22 | | pgpssslw.2 |
. . . . . . . . . . . 12
⊢ 𝑆 = (𝐺 ↾s 𝐻) |
23 | 21, 22 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐻 → (𝐺 ↾s 𝑦) = 𝑆) |
24 | 23 | breq2d 4595 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐻 → (𝑃 pGrp (𝐺 ↾s 𝑦) ↔ 𝑃 pGrp 𝑆)) |
25 | 20, 24 | bitr3d 269 |
. . . . . . . . 9
⊢ (𝑦 = 𝐻 → ((𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦) ↔ 𝑃 pGrp 𝑆)) |
26 | 25 | elrab 3331 |
. . . . . . . 8
⊢ (𝐻 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} ↔ (𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑃 pGrp 𝑆)) |
27 | 17, 18, 26 | sylanbrc 695 |
. . . . . . 7
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → 𝐻 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) |
28 | | fnfvelrn 6264 |
. . . . . . 7
⊢ ((𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} ∧ 𝐻 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (𝐹‘𝐻) ∈ ran 𝐹) |
29 | 16, 27, 28 | sylancr 694 |
. . . . . 6
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (𝐹‘𝐻) ∈ ran 𝐹) |
30 | | ne0i 3880 |
. . . . . 6
⊢ ((𝐹‘𝐻) ∈ ran 𝐹 → ran 𝐹 ≠ ∅) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ran 𝐹 ≠ ∅) |
32 | | hashcl 13009 |
. . . . . . . 8
⊢ (𝑋 ∈ Fin →
(#‘𝑋) ∈
ℕ0) |
33 | 1, 32 | syl 17 |
. . . . . . 7
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (#‘𝑋) ∈
ℕ0) |
34 | 33 | nn0red 11229 |
. . . . . 6
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (#‘𝑋) ∈ ℝ) |
35 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑚 → (#‘𝑥) = (#‘𝑚)) |
36 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(#‘𝑚) ∈
V |
37 | 35, 11, 36 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} → (𝐹‘𝑚) = (#‘𝑚)) |
38 | 37 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (𝐹‘𝑚) = (#‘𝑚)) |
39 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑚 → (𝐺 ↾s 𝑦) = (𝐺 ↾s 𝑚)) |
40 | 39 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑚 → (𝑃 pGrp (𝐺 ↾s 𝑦) ↔ 𝑃 pGrp (𝐺 ↾s 𝑚))) |
41 | | sseq2 3590 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑚 → (𝐻 ⊆ 𝑦 ↔ 𝐻 ⊆ 𝑚)) |
42 | 40, 41 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑚 → ((𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦) ↔ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) |
43 | 42 | elrab 3331 |
. . . . . . . . . 10
⊢ (𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} ↔ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) |
44 | 1 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) → 𝑋 ∈ Fin) |
45 | 3 | subgss 17418 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (SubGrp‘𝐺) → 𝑚 ⊆ 𝑋) |
46 | 45 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) → 𝑚 ⊆ 𝑋) |
47 | | ssdomg 7887 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ Fin → (𝑚 ⊆ 𝑋 → 𝑚 ≼ 𝑋)) |
48 | 44, 46, 47 | sylc 63 |
. . . . . . . . . . 11
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) → 𝑚 ≼ 𝑋) |
49 | | ssfi 8065 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ Fin ∧ 𝑚 ⊆ 𝑋) → 𝑚 ∈ Fin) |
50 | 44, 46, 49 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) → 𝑚 ∈ Fin) |
51 | | hashdom 13029 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ Fin ∧ 𝑋 ∈ Fin) →
((#‘𝑚) ≤
(#‘𝑋) ↔ 𝑚 ≼ 𝑋)) |
52 | 50, 44, 51 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) → ((#‘𝑚) ≤ (#‘𝑋) ↔ 𝑚 ≼ 𝑋)) |
53 | 48, 52 | mpbird 246 |
. . . . . . . . . 10
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚))) → (#‘𝑚) ≤ (#‘𝑋)) |
54 | 43, 53 | sylan2b 491 |
. . . . . . . . 9
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (#‘𝑚) ≤ (#‘𝑋)) |
55 | 38, 54 | eqbrtrd 4605 |
. . . . . . . 8
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (𝐹‘𝑚) ≤ (#‘𝑋)) |
56 | 55 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∀𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑚) ≤ (#‘𝑋)) |
57 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑤 = (𝐹‘𝑚) → (𝑤 ≤ (#‘𝑋) ↔ (𝐹‘𝑚) ≤ (#‘𝑋))) |
58 | 57 | ralrn 6270 |
. . . . . . . 8
⊢ (𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} → (∀𝑤 ∈ ran 𝐹 𝑤 ≤ (#‘𝑋) ↔ ∀𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑚) ≤ (#‘𝑋))) |
59 | 16, 58 | ax-mp 5 |
. . . . . . 7
⊢
(∀𝑤 ∈
ran 𝐹 𝑤 ≤ (#‘𝑋) ↔ ∀𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑚) ≤ (#‘𝑋)) |
60 | 56, 59 | sylibr 223 |
. . . . . 6
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∀𝑤 ∈ ran 𝐹 𝑤 ≤ (#‘𝑋)) |
61 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑧 = (#‘𝑋) → (𝑤 ≤ 𝑧 ↔ 𝑤 ≤ (#‘𝑋))) |
62 | 61 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑧 = (#‘𝑋) → (∀𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧 ↔ ∀𝑤 ∈ ran 𝐹 𝑤 ≤ (#‘𝑋))) |
63 | 62 | rspcev 3282 |
. . . . . 6
⊢
(((#‘𝑋) ∈
ℝ ∧ ∀𝑤
∈ ran 𝐹 𝑤 ≤ (#‘𝑋)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧) |
64 | 34, 60, 63 | syl2anc 691 |
. . . . 5
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧) |
65 | | suprzcl 11333 |
. . . . 5
⊢ ((ran
𝐹 ⊆ ℤ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑧 ∈ ℝ
∀𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧) → sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹) |
66 | 14, 31, 64, 65 | syl3anc 1318 |
. . . 4
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹) |
67 | | fvelrnb 6153 |
. . . . 5
⊢ (𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} → (sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ↔ ∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < ))) |
68 | 16, 67 | ax-mp 5 |
. . . 4
⊢ (sup(ran
𝐹, ℝ, < ) ∈
ran 𝐹 ↔ ∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )) |
69 | 66, 68 | sylib 207 |
. . 3
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )) |
70 | | oveq2 6557 |
. . . . . 6
⊢ (𝑦 = 𝑘 → (𝐺 ↾s 𝑦) = (𝐺 ↾s 𝑘)) |
71 | 70 | breq2d 4595 |
. . . . 5
⊢ (𝑦 = 𝑘 → (𝑃 pGrp (𝐺 ↾s 𝑦) ↔ 𝑃 pGrp (𝐺 ↾s 𝑘))) |
72 | | sseq2 3590 |
. . . . 5
⊢ (𝑦 = 𝑘 → (𝐻 ⊆ 𝑦 ↔ 𝐻 ⊆ 𝑘)) |
73 | 71, 72 | anbi12d 743 |
. . . 4
⊢ (𝑦 = 𝑘 → ((𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦) ↔ (𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘))) |
74 | 73 | rexrab 3337 |
. . 3
⊢
(∃𝑘 ∈
{𝑦 ∈
(SubGrp‘𝐺) ∣
(𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < ) ↔ ∃𝑘 ∈ (SubGrp‘𝐺)((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < ))) |
75 | 69, 74 | sylib 207 |
. 2
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ (SubGrp‘𝐺)((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < ))) |
76 | | simpl3 1059 |
. . . . . . 7
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑃 pGrp 𝑆) |
77 | | pgpprm 17831 |
. . . . . . 7
⊢ (𝑃 pGrp 𝑆 → 𝑃 ∈ ℙ) |
78 | 76, 77 | syl 17 |
. . . . . 6
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑃 ∈
ℙ) |
79 | | simprl 790 |
. . . . . 6
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑘 ∈ (SubGrp‘𝐺)) |
80 | | zssre 11261 |
. . . . . . . . . . . . . . . 16
⊢ ℤ
⊆ ℝ |
81 | 14, 80 | syl6ss 3580 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ran 𝐹 ⊆ ℝ) |
82 | 81 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ran 𝐹 ⊆ ℝ) |
83 | 31 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ran 𝐹 ≠ ∅) |
84 | 64 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧) |
85 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑚 ∈ (SubGrp‘𝐺)) |
86 | | simprrr 801 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑃 pGrp (𝐺 ↾s 𝑚)) |
87 | | simprrl 800 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → (𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘)) |
88 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘)) |
89 | 88 | simprd 478 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝐻 ⊆ 𝑘) |
90 | | simprrl 800 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑘 ⊆ 𝑚) |
91 | 89, 90 | sstrd 3578 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝐻 ⊆ 𝑚) |
92 | 86, 91 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝑃 pGrp (𝐺 ↾s 𝑚) ∧ 𝐻 ⊆ 𝑚)) |
93 | 85, 92, 43 | sylanbrc 695 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) |
94 | 93, 37 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝐹‘𝑚) = (#‘𝑚)) |
95 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 Fn {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} ∧ 𝑚 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) → (𝐹‘𝑚) ∈ ran 𝐹) |
96 | 16, 93, 95 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝐹‘𝑚) ∈ ran 𝐹) |
97 | 94, 96 | eqeltrrd 2689 |
. . . . . . . . . . . . . 14
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (#‘𝑚) ∈ ran 𝐹) |
98 | | suprub 10863 |
. . . . . . . . . . . . . 14
⊢ (((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑧 ∈ ℝ
∀𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧) ∧ (#‘𝑚) ∈ ran 𝐹) → (#‘𝑚) ≤ sup(ran 𝐹, ℝ, < )) |
99 | 82, 83, 84, 97, 98 | syl31anc 1321 |
. . . . . . . . . . . . 13
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (#‘𝑚) ≤ sup(ran 𝐹, ℝ, < )) |
100 | | simprrr 801 |
. . . . . . . . . . . . . . 15
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )) |
101 | 100 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )) |
102 | 79 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑘 ∈ (SubGrp‘𝐺)) |
103 | 73 | elrab 3331 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} ↔ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘))) |
104 | 102, 88, 103 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)}) |
105 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑘 → (#‘𝑥) = (#‘𝑘)) |
106 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(#‘𝑘) ∈
V |
107 | 105, 11, 106 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} → (𝐹‘𝑘) = (#‘𝑘)) |
108 | 104, 107 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝐹‘𝑘) = (#‘𝑘)) |
109 | 101, 108 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → sup(ran 𝐹, ℝ, < ) = (#‘𝑘)) |
110 | 99, 109 | breqtrd 4609 |
. . . . . . . . . . . 12
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (#‘𝑚) ≤ (#‘𝑘)) |
111 | | simpll2 1094 |
. . . . . . . . . . . . . 14
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑋 ∈ Fin) |
112 | 45 | ad2antrl 760 |
. . . . . . . . . . . . . 14
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑚 ⊆ 𝑋) |
113 | 111, 112,
49 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑚 ∈ Fin) |
114 | | ssfi 8065 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ Fin ∧ 𝑘 ⊆ 𝑚) → 𝑘 ∈ Fin) |
115 | 113, 90, 114 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑘 ∈ Fin) |
116 | | hashcl 13009 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ Fin →
(#‘𝑚) ∈
ℕ0) |
117 | | hashcl 13009 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ Fin →
(#‘𝑘) ∈
ℕ0) |
118 | | nn0re 11178 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑚) ∈
ℕ0 → (#‘𝑚) ∈ ℝ) |
119 | | nn0re 11178 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑘) ∈
ℕ0 → (#‘𝑘) ∈ ℝ) |
120 | | lenlt 9995 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝑚) ∈
ℝ ∧ (#‘𝑘)
∈ ℝ) → ((#‘𝑚) ≤ (#‘𝑘) ↔ ¬ (#‘𝑘) < (#‘𝑚))) |
121 | 118, 119,
120 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑚) ∈
ℕ0 ∧ (#‘𝑘) ∈ ℕ0) →
((#‘𝑚) ≤
(#‘𝑘) ↔ ¬
(#‘𝑘) <
(#‘𝑚))) |
122 | 116, 117,
121 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ Fin ∧ 𝑘 ∈ Fin) →
((#‘𝑚) ≤
(#‘𝑘) ↔ ¬
(#‘𝑘) <
(#‘𝑚))) |
123 | 113, 115,
122 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ((#‘𝑚) ≤ (#‘𝑘) ↔ ¬ (#‘𝑘) < (#‘𝑚))) |
124 | 110, 123 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ¬ (#‘𝑘) < (#‘𝑚)) |
125 | | php3 8031 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ Fin ∧ 𝑘 ⊊ 𝑚) → 𝑘 ≺ 𝑚) |
126 | 125 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ Fin → (𝑘 ⊊ 𝑚 → 𝑘 ≺ 𝑚)) |
127 | 113, 126 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝑘 ⊊ 𝑚 → 𝑘 ≺ 𝑚)) |
128 | | hashsdom 13031 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ Fin ∧ 𝑚 ∈ Fin) →
((#‘𝑘) <
(#‘𝑚) ↔ 𝑘 ≺ 𝑚)) |
129 | 115, 113,
128 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ((#‘𝑘) < (#‘𝑚) ↔ 𝑘 ≺ 𝑚)) |
130 | 127, 129 | sylibrd 248 |
. . . . . . . . . . 11
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝑘 ⊊ 𝑚 → (#‘𝑘) < (#‘𝑚))) |
131 | 124, 130 | mtod 188 |
. . . . . . . . . 10
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → ¬ 𝑘 ⊊ 𝑚) |
132 | | sspss 3668 |
. . . . . . . . . . . 12
⊢ (𝑘 ⊆ 𝑚 ↔ (𝑘 ⊊ 𝑚 ∨ 𝑘 = 𝑚)) |
133 | 90, 132 | sylib 207 |
. . . . . . . . . . 11
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (𝑘 ⊊ 𝑚 ∨ 𝑘 = 𝑚)) |
134 | 133 | ord 391 |
. . . . . . . . . 10
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → (¬ 𝑘 ⊊ 𝑚 → 𝑘 = 𝑚)) |
135 | 131, 134 | mpd 15 |
. . . . . . . . 9
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ (𝑚 ∈ (SubGrp‘𝐺) ∧ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) → 𝑘 = 𝑚) |
136 | 135 | expr 641 |
. . . . . . . 8
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → ((𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)) → 𝑘 = 𝑚)) |
137 | 87 | simpld 474 |
. . . . . . . . . 10
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑃 pGrp (𝐺 ↾s 𝑘)) |
138 | 137 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾s 𝑘)) |
139 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝐺 ↾s 𝑘) = (𝐺 ↾s 𝑚)) |
140 | 139 | breq2d 4595 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → (𝑃 pGrp (𝐺 ↾s 𝑘) ↔ 𝑃 pGrp (𝐺 ↾s 𝑚))) |
141 | | eqimss 3620 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → 𝑘 ⊆ 𝑚) |
142 | 141 | biantrurd 528 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → (𝑃 pGrp (𝐺 ↾s 𝑚) ↔ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) |
143 | 140, 142 | bitrd 267 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → (𝑃 pGrp (𝐺 ↾s 𝑘) ↔ (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) |
144 | 138, 143 | syl5ibcom 234 |
. . . . . . . 8
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → (𝑘 = 𝑚 → (𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)))) |
145 | 136, 144 | impbid 201 |
. . . . . . 7
⊢ ((((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) ∧ 𝑚 ∈ (SubGrp‘𝐺)) → ((𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)) ↔ 𝑘 = 𝑚)) |
146 | 145 | ralrimiva 2949 |
. . . . . 6
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → ∀𝑚 ∈ (SubGrp‘𝐺)((𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)) ↔ 𝑘 = 𝑚)) |
147 | | isslw 17846 |
. . . . . 6
⊢ (𝑘 ∈ (𝑃 pSyl 𝐺) ↔ (𝑃 ∈ ℙ ∧ 𝑘 ∈ (SubGrp‘𝐺) ∧ ∀𝑚 ∈ (SubGrp‘𝐺)((𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp (𝐺 ↾s 𝑚)) ↔ 𝑘 = 𝑚))) |
148 | 78, 79, 146, 147 | syl3anbrc 1239 |
. . . . 5
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝑘 ∈ (𝑃 pSyl 𝐺)) |
149 | 87 | simprd 478 |
. . . . 5
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → 𝐻 ⊆ 𝑘) |
150 | 148, 149 | jca 553 |
. . . 4
⊢ (((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )))) → (𝑘 ∈ (𝑃 pSyl 𝐺) ∧ 𝐻 ⊆ 𝑘)) |
151 | 150 | ex 449 |
. . 3
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ((𝑘 ∈ (SubGrp‘𝐺) ∧ ((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < ))) → (𝑘 ∈ (𝑃 pSyl 𝐺) ∧ 𝐻 ⊆ 𝑘))) |
152 | 151 | reximdv2 2997 |
. 2
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → (∃𝑘 ∈ (SubGrp‘𝐺)((𝑃 pGrp (𝐺 ↾s 𝑘) ∧ 𝐻 ⊆ 𝑘) ∧ (𝐹‘𝑘) = sup(ran 𝐹, ℝ, < )) → ∃𝑘 ∈ (𝑃 pSyl 𝐺)𝐻 ⊆ 𝑘)) |
153 | 75, 152 | mpd 15 |
1
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ (𝑃 pSyl 𝐺)𝐻 ⊆ 𝑘) |