Database
GRAPH THEORY
Walks, paths and cycles
Walks as words
wlknwwlksneqs
Metamath Proof Explorer
Description: The set of walks of a fixed length and the set of walks represented by
words have the same size. (Contributed by Alexander van der Vekens , 25-Aug-2018) (Revised by AV , 15-Apr-2021)
Ref
Expression
Assertion
wlknwwlksneqs
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ) = ( ♯ ‘ ( 𝑁 WWalksN 𝐺 ) ) )
Proof
Step
Hyp
Ref
Expression
1
wlknwwlksnen
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ≈ ( 𝑁 WWalksN 𝐺 ) )
2
hasheni
⊢ ( { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ≈ ( 𝑁 WWalksN 𝐺 ) → ( ♯ ‘ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ) = ( ♯ ‘ ( 𝑁 WWalksN 𝐺 ) ) )
3
1 2
syl
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ) = ( ♯ ‘ ( 𝑁 WWalksN 𝐺 ) ) )