Metamath Proof Explorer


Theorem wlknwwlksneqs

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 𝐺 ) ) )