| 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 19616 | . . . . . . 7
⊢ (𝜑 → ((♯‘𝑆) ∈ ℕ ∧ (𝑃 pCnt (♯‘𝑆)) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) | 
| 10 | 9 | simpld 494 | . . . . . 6
⊢ (𝜑 → (♯‘𝑆) ∈
ℕ) | 
| 11 |  | pcndvds 16904 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧
(♯‘𝑆) ∈
ℕ) → ¬ (𝑃↑((𝑃 pCnt (♯‘𝑆)) + 1)) ∥ (♯‘𝑆)) | 
| 12 | 1, 10, 11 | syl2anc 584 | . . . . 5
⊢ (𝜑 → ¬ (𝑃↑((𝑃 pCnt (♯‘𝑆)) + 1)) ∥ (♯‘𝑆)) | 
| 13 | 9 | simprd 495 | . . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (♯‘𝑆)) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) | 
| 14 | 13 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → ((𝑃 pCnt (♯‘𝑆)) + 1) = (((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1)) | 
| 15 | 14 | oveq2d 7447 | . . . . . 6
⊢ (𝜑 → (𝑃↑((𝑃 pCnt (♯‘𝑆)) + 1)) = (𝑃↑(((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1))) | 
| 16 |  | sylow1lem.m | . . . . . . . . 9
⊢  ⊕ =
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) | 
| 17 | 2, 3, 4, 1, 5, 6, 7, 8, 16 | sylow1lem2 19617 | . . . . . . . 8
⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑆)) | 
| 18 |  | sylow1lem3.1 | . . . . . . . . 9
⊢  ∼ =
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑆 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} | 
| 19 | 18, 2 | gaorber 19326 | . . . . . . . 8
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑆) → ∼ Er 𝑆) | 
| 20 | 17, 19 | syl 17 | . . . . . . 7
⊢ (𝜑 → ∼ Er 𝑆) | 
| 21 |  | pwfi 9357 | . . . . . . . . 9
⊢ (𝑋 ∈ Fin ↔ 𝒫
𝑋 ∈
Fin) | 
| 22 | 4, 21 | sylib 218 | . . . . . . . 8
⊢ (𝜑 → 𝒫 𝑋 ∈ Fin) | 
| 23 | 8 | ssrab3 4082 | . . . . . . . 8
⊢ 𝑆 ⊆ 𝒫 𝑋 | 
| 24 |  | ssfi 9213 | . . . . . . . 8
⊢
((𝒫 𝑋 ∈
Fin ∧ 𝑆 ⊆
𝒫 𝑋) → 𝑆 ∈ Fin) | 
| 25 | 22, 23, 24 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → 𝑆 ∈ Fin) | 
| 26 | 20, 25 | qshash 15863 | . . . . . 6
⊢ (𝜑 → (♯‘𝑆) = Σ𝑧 ∈ (𝑆 / ∼
)(♯‘𝑧)) | 
| 27 | 15, 26 | breq12d 5156 | . . . . 5
⊢ (𝜑 → ((𝑃↑((𝑃 pCnt (♯‘𝑆)) + 1)) ∥ (♯‘𝑆) ↔ (𝑃↑(((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1)) ∥ Σ𝑧 ∈ (𝑆 / ∼
)(♯‘𝑧))) | 
| 28 | 12, 27 | mtbid 324 | . . . 4
⊢ (𝜑 → ¬ (𝑃↑(((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1)) ∥ Σ𝑧 ∈ (𝑆 / ∼
)(♯‘𝑧)) | 
| 29 |  | pwfi 9357 | . . . . . . . 8
⊢ (𝑆 ∈ Fin ↔ 𝒫
𝑆 ∈
Fin) | 
| 30 | 25, 29 | sylib 218 | . . . . . . 7
⊢ (𝜑 → 𝒫 𝑆 ∈ Fin) | 
| 31 | 20 | qsss 8818 | . . . . . . 7
⊢ (𝜑 → (𝑆 / ∼ ) ⊆ 𝒫
𝑆) | 
| 32 | 30, 31 | ssfid 9301 | . . . . . 6
⊢ (𝜑 → (𝑆 / ∼ ) ∈
Fin) | 
| 33 | 32 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) → (𝑆 / ∼ ) ∈
Fin) | 
| 34 |  | prmnn 16711 | . . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 35 | 1, 34 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 36 | 1, 10 | pccld 16888 | . . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt (♯‘𝑆)) ∈
ℕ0) | 
| 37 | 13, 36 | eqeltrrd 2842 | . . . . . . . . 9
⊢ (𝜑 → ((𝑃 pCnt (♯‘𝑋)) − 𝑁) ∈
ℕ0) | 
| 38 |  | peano2nn0 12566 | . . . . . . . . 9
⊢ (((𝑃 pCnt (♯‘𝑋)) − 𝑁) ∈ ℕ0 → (((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1) ∈
ℕ0) | 
| 39 | 37, 38 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1) ∈
ℕ0) | 
| 40 | 35, 39 | nnexpcld 14284 | . . . . . . 7
⊢ (𝜑 → (𝑃↑(((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1)) ∈ ℕ) | 
| 41 | 40 | nnzd 12640 | . . . . . 6
⊢ (𝜑 → (𝑃↑(((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1)) ∈ ℤ) | 
| 42 | 41 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) → (𝑃↑(((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1)) ∈ ℤ) | 
| 43 |  | erdm 8755 | . . . . . . . . . 10
⊢ ( ∼ Er
𝑆 → dom ∼ =
𝑆) | 
| 44 | 20, 43 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → dom ∼ = 𝑆) | 
| 45 |  | elqsn0 8826 | . . . . . . . . 9
⊢ ((dom
∼
= 𝑆 ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑧 ≠ ∅) | 
| 46 | 44, 45 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑧 ≠ ∅) | 
| 47 | 25 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑆 ∈ Fin) | 
| 48 | 31 | sselda 3983 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑧 ∈ 𝒫 𝑆) | 
| 49 | 48 | elpwid 4609 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑧 ⊆ 𝑆) | 
| 50 | 47, 49 | ssfid 9301 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑧 ∈ Fin) | 
| 51 |  | hashnncl 14405 | . . . . . . . . 9
⊢ (𝑧 ∈ Fin →
((♯‘𝑧) ∈
ℕ ↔ 𝑧 ≠
∅)) | 
| 52 | 50, 51 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) →
((♯‘𝑧) ∈
ℕ ↔ 𝑧 ≠
∅)) | 
| 53 | 46, 52 | mpbird 257 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 / ∼ )) →
(♯‘𝑧) ∈
ℕ) | 
| 54 | 53 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) →
(♯‘𝑧) ∈
ℕ) | 
| 55 | 54 | nnzd 12640 | . . . . 5
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) →
(♯‘𝑧) ∈
ℤ) | 
| 56 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑎 = 𝑧 → (♯‘𝑎) = (♯‘𝑧)) | 
| 57 | 56 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝑧 → (𝑃 pCnt (♯‘𝑎)) = (𝑃 pCnt (♯‘𝑧))) | 
| 58 | 57 | breq1d 5153 | . . . . . . . . . . 11
⊢ (𝑎 = 𝑧 → ((𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁) ↔ (𝑃 pCnt (♯‘𝑧)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) | 
| 59 | 58 | notbid 318 | . . . . . . . . . 10
⊢ (𝑎 = 𝑧 → (¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁) ↔ ¬ (𝑃 pCnt (♯‘𝑧)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) | 
| 60 | 59 | rspccva 3621 | . . . . . . . . 9
⊢
((∀𝑎 ∈
(𝑆 / ∼ )
¬ (𝑃 pCnt
(♯‘𝑎)) ≤
((𝑃 pCnt
(♯‘𝑋)) −
𝑁) ∧ 𝑧 ∈ (𝑆 / ∼ )) → ¬
(𝑃 pCnt
(♯‘𝑧)) ≤
((𝑃 pCnt
(♯‘𝑋)) −
𝑁)) | 
| 61 | 60 | adantll 714 | . . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → ¬
(𝑃 pCnt
(♯‘𝑧)) ≤
((𝑃 pCnt
(♯‘𝑋)) −
𝑁)) | 
| 62 | 2 | grpbn0 18984 | . . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) | 
| 63 | 3, 62 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ≠ ∅) | 
| 64 |  | hashnncl 14405 | . . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ Fin →
((♯‘𝑋) ∈
ℕ ↔ 𝑋 ≠
∅)) | 
| 65 | 4, 64 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) | 
| 66 | 63, 65 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘𝑋) ∈
ℕ) | 
| 67 | 1, 66 | pccld 16888 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 pCnt (♯‘𝑋)) ∈
ℕ0) | 
| 68 | 67 | nn0zd 12639 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 pCnt (♯‘𝑋)) ∈ ℤ) | 
| 69 | 5 | nn0zd 12639 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 70 | 68, 69 | zsubcld 12727 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 pCnt (♯‘𝑋)) − 𝑁) ∈ ℤ) | 
| 71 | 70 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → ((𝑃 pCnt (♯‘𝑋)) − 𝑁) ∈ ℤ) | 
| 72 | 71 | zred 12722 | . . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → ((𝑃 pCnt (♯‘𝑋)) − 𝑁) ∈ ℝ) | 
| 73 | 1 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → 𝑃 ∈
ℙ) | 
| 74 | 73, 54 | pccld 16888 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (𝑃 pCnt (♯‘𝑧)) ∈
ℕ0) | 
| 75 | 74 | nn0zd 12639 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (𝑃 pCnt (♯‘𝑧)) ∈
ℤ) | 
| 76 | 75 | zred 12722 | . . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (𝑃 pCnt (♯‘𝑧)) ∈
ℝ) | 
| 77 | 72, 76 | ltnled 11408 | . . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (((𝑃 pCnt (♯‘𝑋)) − 𝑁) < (𝑃 pCnt (♯‘𝑧)) ↔ ¬ (𝑃 pCnt (♯‘𝑧)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) | 
| 78 | 61, 77 | mpbird 257 | . . . . . . 7
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → ((𝑃 pCnt (♯‘𝑋)) − 𝑁) < (𝑃 pCnt (♯‘𝑧))) | 
| 79 |  | zltp1le 12667 | . . . . . . . 8
⊢ ((((𝑃 pCnt (♯‘𝑋)) − 𝑁) ∈ ℤ ∧ (𝑃 pCnt (♯‘𝑧)) ∈ ℤ) → (((𝑃 pCnt (♯‘𝑋)) − 𝑁) < (𝑃 pCnt (♯‘𝑧)) ↔ (((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1) ≤ (𝑃 pCnt (♯‘𝑧)))) | 
| 80 | 71, 75, 79 | syl2anc 584 | . . . . . . 7
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (((𝑃 pCnt (♯‘𝑋)) − 𝑁) < (𝑃 pCnt (♯‘𝑧)) ↔ (((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1) ≤ (𝑃 pCnt (♯‘𝑧)))) | 
| 81 | 78, 80 | mpbid 232 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1) ≤ (𝑃 pCnt (♯‘𝑧))) | 
| 82 | 39 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1) ∈
ℕ0) | 
| 83 |  | pcdvdsb 16907 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧
(♯‘𝑧) ∈
ℤ ∧ (((𝑃 pCnt
(♯‘𝑋)) −
𝑁) + 1) ∈
ℕ0) → ((((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1) ≤ (𝑃 pCnt (♯‘𝑧)) ↔ (𝑃↑(((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1)) ∥ (♯‘𝑧))) | 
| 84 | 73, 55, 82, 83 | syl3anc 1373 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → ((((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1) ≤ (𝑃 pCnt (♯‘𝑧)) ↔ (𝑃↑(((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1)) ∥ (♯‘𝑧))) | 
| 85 | 81, 84 | mpbid 232 | . . . . 5
⊢ (((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ∧ 𝑧 ∈ (𝑆 / ∼ )) → (𝑃↑(((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1)) ∥ (♯‘𝑧)) | 
| 86 | 33, 42, 55, 85 | fsumdvds 16345 | . . . 4
⊢ ((𝜑 ∧ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) → (𝑃↑(((𝑃 pCnt (♯‘𝑋)) − 𝑁) + 1)) ∥ Σ𝑧 ∈ (𝑆 / ∼
)(♯‘𝑧)) | 
| 87 | 28, 86 | mtand 816 | . . 3
⊢ (𝜑 → ¬ ∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) | 
| 88 |  | dfrex2 3073 | . . 3
⊢
(∃𝑎 ∈
(𝑆 / ∼
)(𝑃 pCnt
(♯‘𝑎)) ≤
((𝑃 pCnt
(♯‘𝑋)) −
𝑁) ↔ ¬
∀𝑎 ∈ (𝑆 / ∼ ) ¬ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) | 
| 89 | 87, 88 | sylibr 234 | . 2
⊢ (𝜑 → ∃𝑎 ∈ (𝑆 / ∼ )(𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) | 
| 90 |  | eqid 2737 | . . . 4
⊢ (𝑆 / ∼ ) = (𝑆 / ∼ ) | 
| 91 |  | fveq2 6906 | . . . . . . 7
⊢ ([𝑧] ∼ = 𝑎 → (♯‘[𝑧] ∼ ) =
(♯‘𝑎)) | 
| 92 | 91 | oveq2d 7447 | . . . . . 6
⊢ ([𝑧] ∼ = 𝑎 → (𝑃 pCnt (♯‘[𝑧] ∼ )) = (𝑃 pCnt (♯‘𝑎))) | 
| 93 | 92 | breq1d 5153 | . . . . 5
⊢ ([𝑧] ∼ = 𝑎 → ((𝑃 pCnt (♯‘[𝑧] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁) ↔ (𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) | 
| 94 | 93 | imbi1d 341 | . . . 4
⊢ ([𝑧] ∼ = 𝑎 → (((𝑃 pCnt (♯‘[𝑧] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (♯‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) ↔ ((𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (♯‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)))) | 
| 95 |  | eceq1 8784 | . . . . . . . . . 10
⊢ (𝑤 = 𝑧 → [𝑤] ∼ = [𝑧] ∼ ) | 
| 96 | 95 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝑤 = 𝑧 → (♯‘[𝑤] ∼ ) =
(♯‘[𝑧] ∼
)) | 
| 97 | 96 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑤 = 𝑧 → (𝑃 pCnt (♯‘[𝑤] ∼ )) = (𝑃 pCnt (♯‘[𝑧] ∼
))) | 
| 98 | 97 | breq1d 5153 | . . . . . . 7
⊢ (𝑤 = 𝑧 → ((𝑃 pCnt (♯‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁) ↔ (𝑃 pCnt (♯‘[𝑧] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) | 
| 99 | 98 | rspcev 3622 | . . . . . 6
⊢ ((𝑧 ∈ 𝑆 ∧ (𝑃 pCnt (♯‘[𝑧] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (♯‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) | 
| 100 | 99 | ex 412 | . . . . 5
⊢ (𝑧 ∈ 𝑆 → ((𝑃 pCnt (♯‘[𝑧] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (♯‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) | 
| 101 | 100 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝑃 pCnt (♯‘[𝑧] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (♯‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) | 
| 102 | 90, 94, 101 | ectocld 8824 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑆 / ∼ )) → ((𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (♯‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) | 
| 103 | 102 | rexlimdva 3155 | . 2
⊢ (𝜑 → (∃𝑎 ∈ (𝑆 / ∼ )(𝑃 pCnt (♯‘𝑎)) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁) → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (♯‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) | 
| 104 | 89, 103 | mpd 15 | 1
⊢ (𝜑 → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (♯‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) |