Step |
Hyp |
Ref |
Expression |
1 |
|
rusgrnumwwlkg.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
ovex |
⊢ ( 𝑁 WWalksN 𝐺 ) ∈ V |
3 |
2
|
rabex |
⊢ { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } ∈ V |
4 |
|
rusgrusgr |
⊢ ( 𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph ) |
5 |
|
usgruspgr |
⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph ) |
6 |
4 5
|
syl |
⊢ ( 𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USPGraph ) |
7 |
|
simp3 |
⊢ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 ) |
8 |
|
wlksnwwlknvbij |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑃 ) } –1-1-onto→ { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } ) |
9 |
6 7 8
|
syl2an |
⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑃 ) } –1-1-onto→ { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } ) |
10 |
|
f1oexbi |
⊢ ( ∃ 𝑔 𝑔 : { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } –1-1-onto→ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑃 ) } ↔ ∃ 𝑓 𝑓 : { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑃 ) } –1-1-onto→ { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } ) |
11 |
9 10
|
sylibr |
⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ∃ 𝑔 𝑔 : { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } –1-1-onto→ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑃 ) } ) |
12 |
|
hasheqf1oi |
⊢ ( { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } ∈ V → ( ∃ 𝑔 𝑔 : { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } –1-1-onto→ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑃 ) } → ( ♯ ‘ { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } ) = ( ♯ ‘ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑃 ) } ) ) ) |
13 |
3 11 12
|
mpsyl |
⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } ) = ( ♯ ‘ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑃 ) } ) ) |
14 |
1
|
rusgrnumwwlkg |
⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) |
15 |
13 14
|
eqtr3d |
⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑃 ) } ) = ( 𝐾 ↑ 𝑁 ) ) |