wlksnwwlknvbij

Description: There is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length and starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 5-Aug-2022)

		Ref	Expression
	Assertion	wlksnwwlknvbij	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ∃ 𝑓 𝑓 : { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 ) } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( Walks ‘ 𝐺 ) ∈ V
2	1	mptrabex	⊢ ( 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑝 ) ) ∈ V
3	2	resex	⊢ ( ( 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } ) ∈ V
4		eqid	⊢ ( 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑝 ) ) = ( 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑝 ) )
5		eqid	⊢ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } = { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 }
6		eqid	⊢ ( 𝑁 WWalksN 𝐺 ) = ( 𝑁 WWalksN 𝐺 )
7	5 6 4	wlknwwlksnbij	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑝 ) ) : { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } –1-1-onto→ ( 𝑁 WWalksN 𝐺 ) )
8		fveq1	⊢ ( 𝑤 = ( 2^nd ‘ 𝑝 ) → ( 𝑤 ‘ 0 ) = ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) )
9	8	eqeq1d	⊢ ( 𝑤 = ( 2^nd ‘ 𝑝 ) → ( ( 𝑤 ‘ 0 ) = 𝑋 ↔ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 ) )
10	9	3ad2ant3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∧ 𝑤 = ( 2^nd ‘ 𝑝 ) ) → ( ( 𝑤 ‘ 0 ) = 𝑋 ↔ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 ) )
11	4 7 10	f1oresrab	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( ( 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } ) : { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
12		f1oeq1	⊢ ( 𝑓 = ( ( 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } ) → ( 𝑓 : { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ↔ ( ( 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } ) : { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) )
13	12	spcegv	⊢ ( ( ( 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } ) ∈ V → ( ( ( 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } ) : { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } → ∃ 𝑓 𝑓 : { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) )
14	3 11 13	mpsyl	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ∃ 𝑓 𝑓 : { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
15		2fveq3	⊢ ( 𝑝 = 𝑞 → ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) )
16	15	eqeq1d	⊢ ( 𝑝 = 𝑞 → ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ↔ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 ) )
17	16	rabrabi	⊢ { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } = { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 ) }
18	17	eqcomi	⊢ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 ) } = { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 }
19		f1oeq2	⊢ ( { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 ) } = { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } → ( 𝑓 : { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 ) } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ↔ 𝑓 : { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) )
20	18 19	mp1i	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( 𝑓 : { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 ) } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ↔ 𝑓 : { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) )
21	20	exbidv	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( ∃ 𝑓 𝑓 : { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 ) } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ↔ ∃ 𝑓 𝑓 : { 𝑝 ∈ { 𝑞 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑞 ) ) = 𝑁 } ∣ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) )
22	14 21	mpbird	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ∃ 𝑓 𝑓 : { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑝 ) ‘ 0 ) = 𝑋 ) } –1-1-onto→ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )

Metamath Proof Explorer

Theorem wlksnwwlknvbij

Proof