Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
2 |
1
|
fusgrvtxfi |
⊢ ( 𝐺 ∈ FinUSGraph → ( Vtx ‘ 𝐺 ) ∈ Fin ) |
3 |
2
|
adantr |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0 ) → ( Vtx ‘ 𝐺 ) ∈ Fin ) |
4 |
|
wwlksnfi |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WWalksN 𝐺 ) ∈ Fin ) |
5 |
3 4
|
syl |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 WWalksN 𝐺 ) ∈ Fin ) |
6 |
|
fusgrusgr |
⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph ) |
7 |
|
usgruspgr |
⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph ) |
8 |
6 7
|
syl |
⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USPGraph ) |
9 |
|
wlknwwlksnen |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ≈ ( 𝑁 WWalksN 𝐺 ) ) |
10 |
8 9
|
sylan |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0 ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ≈ ( 𝑁 WWalksN 𝐺 ) ) |
11 |
|
enfii |
⊢ ( ( ( 𝑁 WWalksN 𝐺 ) ∈ Fin ∧ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ≈ ( 𝑁 WWalksN 𝐺 ) ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ∈ Fin ) |
12 |
5 10 11
|
syl2anc |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0 ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ∈ Fin ) |