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 ∧ 𝑁 ∈ ℕ₀ ) → ( ♯ ‘ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ) = ( ♯ ‘ ( 𝑁 WWalksN 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		wlknwwlksnen	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ≈ ( 𝑁 WWalksN 𝐺 ) )
2		hasheni	⊢ ( { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ≈ ( 𝑁 WWalksN 𝐺 ) → ( ♯ ‘ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ) = ( ♯ ‘ ( 𝑁 WWalksN 𝐺 ) ) )
3	1 2	syl	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( ♯ ‘ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ) = ( ♯ ‘ ( 𝑁 WWalksN 𝐺 ) ) )

Metamath Proof Explorer

Theorem wlknwwlksneqs

Proof