Step |
Hyp |
Ref |
Expression |
1 |
|
numclwwlk.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
numclwwlk.q |
⊢ 𝑄 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } ) |
3 |
1 2
|
numclwwlkovq |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 𝑄 𝑁 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) |
4 |
3
|
adantl |
⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑋 𝑄 𝑁 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) |
5 |
4
|
fveq2d |
⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ♯ ‘ ( 𝑋 𝑄 𝑁 ) ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) ) |
6 |
|
nnnn0 |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 ) |
7 |
|
eqid |
⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } |
8 |
|
eqid |
⊢ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) = ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) |
9 |
7 8 1
|
clwwlknclwwlkdifnum |
⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) = ( ( 𝐾 ↑ 𝑁 ) − ( ♯ ‘ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) ) ) ) |
10 |
6 9
|
sylanr2 |
⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) = ( ( 𝐾 ↑ 𝑁 ) − ( ♯ ‘ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) ) ) ) |
11 |
1
|
iswwlksnon |
⊢ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) } |
12 |
|
wwlknlsw |
⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑤 ‘ 𝑁 ) = ( lastS ‘ 𝑤 ) ) |
13 |
|
eqcom |
⊢ ( ( 𝑤 ‘ 0 ) = 𝑋 ↔ 𝑋 = ( 𝑤 ‘ 0 ) ) |
14 |
13
|
biimpi |
⊢ ( ( 𝑤 ‘ 0 ) = 𝑋 → 𝑋 = ( 𝑤 ‘ 0 ) ) |
15 |
12 14
|
eqeqan12d |
⊢ ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( ( 𝑤 ‘ 𝑁 ) = 𝑋 ↔ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ) |
16 |
15
|
pm5.32da |
⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) ↔ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ) ) |
17 |
16
|
biancomd |
⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) ↔ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) ) |
18 |
17
|
rabbiia |
⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑋 ) } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } |
19 |
11 18
|
eqtri |
⊢ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } |
20 |
19
|
fveq2i |
⊢ ( ♯ ‘ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) |
21 |
20
|
a1i |
⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ♯ ‘ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) ) |
22 |
21
|
oveq2d |
⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝐾 ↑ 𝑁 ) − ( ♯ ‘ ( 𝑋 ( 𝑁 WWalksNOn 𝐺 ) 𝑋 ) ) ) = ( ( 𝐾 ↑ 𝑁 ) − ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) ) ) |
23 |
10 22
|
eqtrd |
⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) = ( ( 𝐾 ↑ 𝑁 ) − ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) ) ) |
24 |
|
ovex |
⊢ ( 𝑁 WWalksN 𝐺 ) ∈ V |
25 |
24
|
rabex |
⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ∈ V |
26 |
|
clwwlkvbij |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) |
27 |
26
|
adantl |
⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) |
28 |
|
hasheqf1oi |
⊢ ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ∈ V → ( ∃ 𝑓 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) = ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) ) ) |
29 |
25 27 28
|
mpsyl |
⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) = ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) ) |
30 |
29
|
oveq2d |
⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝐾 ↑ 𝑁 ) − ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } ) ) = ( ( 𝐾 ↑ 𝑁 ) − ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) ) ) |
31 |
5 23 30
|
3eqtrd |
⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ♯ ‘ ( 𝑋 𝑄 𝑁 ) ) = ( ( 𝐾 ↑ 𝑁 ) − ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) ) ) |