Metamath Proof Explorer

Theorem wlknwwlksnen

Description: In a simple pseudograph, the set of walks of a fixed length and the set of walks represented by words are equinumerous. (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 5-Aug-2022)

		Ref	Expression
	Assertion	wlknwwlksnen	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ≈ ( 𝑁 WWalksN 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } = { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 }
2		eqid	⊢ ( 𝑁 WWalksN 𝐺 ) = ( 𝑁 WWalksN 𝐺 )
3		eqid	⊢ ( 𝑤 ∈ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑤 ) ) = ( 𝑤 ∈ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑤 ) )
4	1 2 3	wlknwwlksnbij	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( 𝑤 ∈ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑤 ) ) : { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } –1-1-onto→ ( 𝑁 WWalksN 𝐺 ) )
5		fvex	⊢ ( Walks ‘ 𝐺 ) ∈ V
6	5	rabex	⊢ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ∈ V
7	6	f1oen	⊢ ( ( 𝑤 ∈ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑤 ) ) : { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } –1-1-onto→ ( 𝑁 WWalksN 𝐺 ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ≈ ( 𝑁 WWalksN 𝐺 ) )
8	4 7	syl	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ≈ ( 𝑁 WWalksN 𝐺 ) )