Step |
Hyp |
Ref |
Expression |
1 |
|
sylow1.x |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
sylow1.g |
⊢ ( 𝜑 → 𝐺 ∈ Grp ) |
3 |
|
sylow1.f |
⊢ ( 𝜑 → 𝑋 ∈ Fin ) |
4 |
|
sylow1.p |
⊢ ( 𝜑 → 𝑃 ∈ ℙ ) |
5 |
|
sylow1.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
6 |
|
sylow1.d |
⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) ) |
7 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
8 |
|
eqid |
⊢ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } = { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } |
9 |
|
oveq2 |
⊢ ( 𝑠 = 𝑧 → ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) = ( 𝑢 ( +g ‘ 𝐺 ) 𝑧 ) ) |
10 |
9
|
cbvmptv |
⊢ ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) = ( 𝑧 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑧 ) ) |
11 |
|
oveq1 |
⊢ ( 𝑢 = 𝑥 → ( 𝑢 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) |
12 |
11
|
mpteq2dv |
⊢ ( 𝑢 = 𝑥 → ( 𝑧 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) ) |
13 |
10 12
|
eqtrid |
⊢ ( 𝑢 = 𝑥 → ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) = ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) ) |
14 |
13
|
rneqd |
⊢ ( 𝑢 = 𝑥 → ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) = ran ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) ) |
15 |
|
mpteq1 |
⊢ ( 𝑣 = 𝑦 → ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) ) |
16 |
15
|
rneqd |
⊢ ( 𝑣 = 𝑦 → ran ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) = ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) ) |
17 |
14 16
|
cbvmpov |
⊢ ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ) ) |
18 |
|
preq12 |
⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → { 𝑎 , 𝑏 } = { 𝑥 , 𝑦 } ) |
19 |
18
|
sseq1d |
⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↔ { 𝑥 , 𝑦 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ) ) |
20 |
|
oveq2 |
⊢ ( 𝑎 = 𝑥 → ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑥 ) ) |
21 |
|
id |
⊢ ( 𝑏 = 𝑦 → 𝑏 = 𝑦 ) |
22 |
20 21
|
eqeqan12d |
⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ↔ ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑥 ) = 𝑦 ) ) |
23 |
22
|
rexbidv |
⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ↔ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑥 ) = 𝑦 ) ) |
24 |
19 23
|
anbi12d |
⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) ↔ ( { 𝑥 , 𝑦 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑥 ) = 𝑦 ) ) ) |
25 |
24
|
cbvopabv |
⊢ { 〈 𝑎 , 𝑏 〉 ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑥 ) = 𝑦 ) } |
26 |
1 2 3 4 5 6 7 8 17 25
|
sylow1lem3 |
⊢ ( 𝜑 → ∃ ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { 〈 𝑎 , 𝑏 〉 ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) |
27 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { 〈 𝑎 , 𝑏 〉 ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → 𝐺 ∈ Grp ) |
28 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { 〈 𝑎 , 𝑏 〉 ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → 𝑋 ∈ Fin ) |
29 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { 〈 𝑎 , 𝑏 〉 ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → 𝑃 ∈ ℙ ) |
30 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { 〈 𝑎 , 𝑏 〉 ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → 𝑁 ∈ ℕ0 ) |
31 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { 〈 𝑎 , 𝑏 〉 ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) ) |
32 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { 〈 𝑎 , 𝑏 〉 ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ) |
33 |
|
eqid |
⊢ { 𝑡 ∈ 𝑋 ∣ ( 𝑡 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) ℎ ) = ℎ } = { 𝑡 ∈ 𝑋 ∣ ( 𝑡 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) ℎ ) = ℎ } |
34 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { 〈 𝑎 , 𝑏 〉 ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { 〈 𝑎 , 𝑏 〉 ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) |
35 |
1 27 28 29 30 31 7 8 17 25 32 33 34
|
sylow1lem5 |
⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { 〈 𝑎 , 𝑏 〉 ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → ∃ 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑔 ) = ( 𝑃 ↑ 𝑁 ) ) |
36 |
26 35
|
rexlimddv |
⊢ ( 𝜑 → ∃ 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑔 ) = ( 𝑃 ↑ 𝑁 ) ) |