Step | Hyp | Ref
| Expression |
1 | | sylow1.p |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℙ) |
2 | | sylow1.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
3 | | sylow1.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Grp) |
4 | | sylow1.f |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ Fin) |
5 | | sylow1.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
6 | | sylow1.d |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑𝑁) ∥ (#‘𝑋)) |
7 | | sylow1lem.a |
. . . . . . . 8
⊢ + =
(+g‘𝐺) |
8 | | sylow1lem.s |
. . . . . . . 8
⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)} |
9 | 2, 3, 4, 1, 5, 6, 7, 8 | sylow1lem1 18013 |
. . . . . . 7
⊢ (𝜑 → ((#‘𝑆) ∈ ℕ ∧ (𝑃 pCnt (#‘𝑆)) = ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
10 | 9 | simpld 475 |
. . . . . 6
⊢ (𝜑 → (#‘𝑆) ∈ ℕ) |
11 | | pcndvds 15570 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧
(#‘𝑆) ∈ ℕ)
→ ¬ (𝑃↑((𝑃 pCnt (#‘𝑆)) + 1)) ∥ (#‘𝑆)) |
12 | 1, 10, 11 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ¬ (𝑃↑((𝑃 pCnt (#‘𝑆)) + 1)) ∥ (#‘𝑆)) |
13 | 9 | simprd 479 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (#‘𝑆)) = ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
14 | 13 | oveq1d 6665 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 pCnt (#‘𝑆)) + 1) = (((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1)) |
15 | 14 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → (𝑃↑((𝑃 pCnt (#‘𝑆)) + 1)) = (𝑃↑(((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1))) |
16 | | sylow1lem.m |
. . . . . . . . 9
⊢ ⊕ =
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
17 | 2, 3, 4, 1, 5, 6, 7, 8, 16 | sylow1lem2 18014 |
. . . . . . . 8
⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑆)) |
18 | | sylow1lem3.1 |
. . . . . . . . 9
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑆 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} |
19 | 18, 2 | gaorber 17741 |
. . . . . . . 8
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑆) → ∼ Er 𝑆) |
20 | 17, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ∼ Er 𝑆) |
21 | | pwfi 8261 |
. . . . . . . . 9
⊢ (𝑋 ∈ Fin ↔ 𝒫
𝑋 ∈
Fin) |
22 | 4, 21 | sylib 208 |
. . . . . . . 8
⊢ (𝜑 → 𝒫 𝑋 ∈ Fin) |
23 | | ssrab2 3687 |
. . . . . . . . 9
⊢ {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)} ⊆ 𝒫 𝑋 |
24 | 8, 23 | eqsstri 3635 |
. . . . . . . 8
⊢ 𝑆 ⊆ 𝒫 𝑋 |
25 | | ssfi 8180 |
. . . . . . . 8
⊢
((𝒫 𝑋 ∈
Fin ∧ 𝑆 ⊆
𝒫 𝑋) → 𝑆 ∈ Fin) |
26 | 22, 24, 25 | sylancl 694 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ Fin) |
27 | 20, 26 | qshash 14559 |
. . . . . 6
⊢ (𝜑 → (#‘𝑆) = Σ𝑧 ∈ (𝑆 / ∼ )(#‘𝑧)) |
28 | 15, 27 | breq12d 4666 |
. . . . 5
⊢ (𝜑 → ((𝑃↑((𝑃 pCnt (#‘𝑆)) + 1)) ∥ (#‘𝑆) ↔ (𝑃↑(((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1)) ∥ Σ𝑧 ∈ (𝑆 / ∼ )(#‘𝑧))) |
29 | 12, 28 | mtbid 314 |
. . . 4
⊢ (𝜑 → ¬ (𝑃↑(((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1)) ∥ Σ𝑧 ∈ (𝑆 / ∼ )(#‘𝑧)) |
30 | | pwfi 8261 |
. . . . . . . 8
⊢ (𝑆 ∈ Fin ↔ 𝒫
𝑆 ∈
Fin) |
31 | 26, 30 | sylib 208 |
. . . . . . 7
⊢ (𝜑 → 𝒫 𝑆 ∈ Fin) |
32 | 20 | qsss 7808 |
. . . . . . 7
⊢ (𝜑 → (𝑆 / ∼ ) ⊆ 𝒫
𝑆) |
33 | | ssfi 8180 |
. . . . . . 7
⊢
((𝒫 𝑆 ∈
Fin ∧ (𝑆 / ∼ )
⊆ 𝒫 𝑆) →
(𝑆 / ∼ )
∈ Fin) |
34 | 31, 32, 33 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝑆 / ∼ ) ∈
Fin) |
35 | 34 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) → (𝑆 / ∼ ) ∈
Fin) |
36 | | prmnn 15388 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
37 | 1, 36 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℕ) |
38 | 1, 10 | pccld 15555 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt (#‘𝑆)) ∈
ℕ0) |
39 | 13, 38 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 pCnt (#‘𝑋)) − 𝑁) ∈
ℕ0) |
40 | | peano2nn0 11333 |
. . . . . . . . 9
⊢ (((𝑃 pCnt (#‘𝑋)) − 𝑁) ∈ ℕ0 → (((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1) ∈
ℕ0) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1) ∈
ℕ0) |
42 | 37, 41 | nnexpcld 13030 |
. . . . . . 7
⊢ (𝜑 → (𝑃↑(((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1)) ∈ ℕ) |
43 | 42 | nnzd 11481 |
. . . . . 6
⊢ (𝜑 → (𝑃↑(((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1)) ∈ ℤ) |
44 | 43 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) → (𝑃↑(((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1)) ∈ ℤ) |
45 | | erdm 7752 |
. . . . . . . . . 10
⊢ ( ∼ Er
𝑆 → dom ∼ =
𝑆) |
46 | 20, 45 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom ∼ = 𝑆) |
47 | | elqsn0 7816 |
. . . . . . . . 9
⊢ ((dom
∼
= 𝑆 ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑧 ≠ ∅) |
48 | 46, 47 | sylan 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑧 ≠ ∅) |
49 | 26 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑆 ∈ Fin) |
50 | 32 | sselda 3603 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑧 ∈ 𝒫 𝑆) |
51 | 50 | elpwid 4170 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑧 ⊆ 𝑆) |
52 | | ssfi 8180 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Fin ∧ 𝑧 ⊆ 𝑆) → 𝑧 ∈ Fin) |
53 | 49, 51, 52 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑧 ∈ Fin) |
54 | | hashnncl 13157 |
. . . . . . . . 9
⊢ (𝑧 ∈ Fin →
((#‘𝑧) ∈ ℕ
↔ 𝑧 ≠
∅)) |
55 | 53, 54 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) →
((#‘𝑧) ∈ ℕ
↔ 𝑧 ≠
∅)) |
56 | 48, 55 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) →
(#‘𝑧) ∈
ℕ) |
57 | 56 | adantlr 751 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) →
(#‘𝑧) ∈
ℕ) |
58 | 57 | nnzd 11481 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) →
(#‘𝑧) ∈
ℤ) |
59 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑧 → (#‘𝑎) = (#‘𝑧)) |
60 | 59 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑧 → (𝑃 pCnt (#‘𝑎)) = (𝑃 pCnt (#‘𝑧))) |
61 | 60 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑧 → ((𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁) ↔ (𝑃 pCnt (#‘𝑧)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
62 | 61 | notbid 308 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑧 → (¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁) ↔ ¬ (𝑃 pCnt (#‘𝑧)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
63 | 62 | rspccva 3308 |
. . . . . . . . 9
⊢
((∀𝑎 ∈
(𝑆 / ∼ )
¬ (𝑃 pCnt
(#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁) ∧ 𝑧 ∈ (𝑆 / ∼ )) → ¬
(𝑃 pCnt (#‘𝑧)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
64 | 63 | adantll 750 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → ¬
(𝑃 pCnt (#‘𝑧)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
65 | 2 | grpbn0 17451 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) |
66 | 3, 65 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ≠ ∅) |
67 | | hashnncl 13157 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ Fin →
((#‘𝑋) ∈ ℕ
↔ 𝑋 ≠
∅)) |
68 | 4, 67 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) |
69 | 66, 68 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (#‘𝑋) ∈ ℕ) |
70 | 1, 69 | pccld 15555 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 pCnt (#‘𝑋)) ∈
ℕ0) |
71 | 70 | nn0zd 11480 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 pCnt (#‘𝑋)) ∈ ℤ) |
72 | 5 | nn0zd 11480 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) |
73 | 71, 72 | zsubcld 11487 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 pCnt (#‘𝑋)) − 𝑁) ∈ ℤ) |
74 | 73 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → ((𝑃 pCnt (#‘𝑋)) − 𝑁) ∈ ℤ) |
75 | 74 | zred 11482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → ((𝑃 pCnt (#‘𝑋)) − 𝑁) ∈ ℝ) |
76 | 1 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑃 ∈
ℙ) |
77 | 76, 57 | pccld 15555 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (𝑃 pCnt (#‘𝑧)) ∈
ℕ0) |
78 | 77 | nn0zd 11480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (𝑃 pCnt (#‘𝑧)) ∈
ℤ) |
79 | 78 | zred 11482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (𝑃 pCnt (#‘𝑧)) ∈
ℝ) |
80 | 75, 79 | ltnled 10184 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (((𝑃 pCnt (#‘𝑋)) − 𝑁) < (𝑃 pCnt (#‘𝑧)) ↔ ¬ (𝑃 pCnt (#‘𝑧)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
81 | 64, 80 | mpbird 247 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → ((𝑃 pCnt (#‘𝑋)) − 𝑁) < (𝑃 pCnt (#‘𝑧))) |
82 | | zltp1le 11427 |
. . . . . . . 8
⊢ ((((𝑃 pCnt (#‘𝑋)) − 𝑁) ∈ ℤ ∧ (𝑃 pCnt (#‘𝑧)) ∈ ℤ) → (((𝑃 pCnt (#‘𝑋)) − 𝑁) < (𝑃 pCnt (#‘𝑧)) ↔ (((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1) ≤ (𝑃 pCnt (#‘𝑧)))) |
83 | 74, 78, 82 | syl2anc 693 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (((𝑃 pCnt (#‘𝑋)) − 𝑁) < (𝑃 pCnt (#‘𝑧)) ↔ (((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1) ≤ (𝑃 pCnt (#‘𝑧)))) |
84 | 81, 83 | mpbid 222 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1) ≤ (𝑃 pCnt (#‘𝑧))) |
85 | 41 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1) ∈
ℕ0) |
86 | | pcdvdsb 15573 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧
(#‘𝑧) ∈ ℤ
∧ (((𝑃 pCnt
(#‘𝑋)) − 𝑁) + 1) ∈
ℕ0) → ((((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1) ≤ (𝑃 pCnt (#‘𝑧)) ↔ (𝑃↑(((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1)) ∥ (#‘𝑧))) |
87 | 76, 58, 85, 86 | syl3anc 1326 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → ((((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1) ≤ (𝑃 pCnt (#‘𝑧)) ↔ (𝑃↑(((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1)) ∥ (#‘𝑧))) |
88 | 84, 87 | mpbid 222 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (𝑃↑(((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1)) ∥ (#‘𝑧)) |
89 | 35, 44, 58, 88 | fsumdvds 15030 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) → (𝑃↑(((𝑃 pCnt (#‘𝑋)) − 𝑁) + 1)) ∥ Σ𝑧 ∈ (𝑆 / ∼ )(#‘𝑧)) |
90 | 29, 89 | mtand 691 |
. . 3
⊢ (𝜑 → ¬ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
91 | | dfrex2 2996 |
. . 3
⊢
(∃𝑎 ∈
(𝑆 / ∼
)(𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁) ↔ ¬ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
92 | 90, 91 | sylibr 224 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ (𝑆 / ∼ )(𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
93 | | eqid 2622 |
. . . 4
⊢ (𝑆 / ∼ ) = (𝑆 / ∼ ) |
94 | | fveq2 6191 |
. . . . . . 7
⊢ ([𝑧] ∼ = 𝑎 → (#‘[𝑧] ∼ ) = (#‘𝑎)) |
95 | 94 | oveq2d 6666 |
. . . . . 6
⊢ ([𝑧] ∼ = 𝑎 → (𝑃 pCnt (#‘[𝑧] ∼ )) = (𝑃 pCnt (#‘𝑎))) |
96 | 95 | breq1d 4663 |
. . . . 5
⊢ ([𝑧] ∼ = 𝑎 → ((𝑃 pCnt (#‘[𝑧] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁) ↔ (𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
97 | 96 | imbi1d 331 |
. . . 4
⊢ ([𝑧] ∼ = 𝑎 → (((𝑃 pCnt (#‘[𝑧] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (#‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ↔ ((𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (#‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)))) |
98 | | eceq1 7782 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → [𝑤] ∼ = [𝑧] ∼ ) |
99 | 98 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (#‘[𝑤] ∼ ) = (#‘[𝑧] ∼ )) |
100 | 99 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (𝑃 pCnt (#‘[𝑤] ∼ )) = (𝑃 pCnt (#‘[𝑧] ∼
))) |
101 | 100 | breq1d 4663 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → ((𝑃 pCnt (#‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁) ↔ (𝑃 pCnt (#‘[𝑧] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
102 | 101 | rspcev 3309 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑆 ∧ (𝑃 pCnt (#‘[𝑧] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (#‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
103 | 102 | ex 450 |
. . . . 5
⊢ (𝑧 ∈ 𝑆 → ((𝑃 pCnt (#‘[𝑧] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (#‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
104 | 103 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝑃 pCnt (#‘[𝑧] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (#‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
105 | 93, 97, 104 | ectocld 7814 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑆 / ∼ )) → ((𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (#‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
106 | 105 | rexlimdva 3031 |
. 2
⊢ (𝜑 → (∃𝑎 ∈ (𝑆 / ∼ )(𝑃 pCnt (#‘𝑎)) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (#‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
107 | 92, 106 | mpd 15 |
1
⊢ (𝜑 → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (#‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |