Theorem clwwlkf1o

Description: F is a 1-1 onto function, that means that there is a bijection between the set of closed walks of a fixed length represented by walks (as words) and the set of closed walks (as words) of the fixed length. The difference between these two representations is that in the first case the starting vertex is repeated at the end of the word, and in the second case it is not. (Contributed by Alexander van der Vekens, 29-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 1-Nov-2022)

	Ref	Expression
Hypotheses	clwwlkf1o.d	⊢ 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
	clwwlkf1o.f	⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝑡 prefix 𝑁 ) )
Assertion	clwwlkf1o	⊢ ( 𝑁 ∈ ℕ → 𝐹 : 𝐷 –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		clwwlkf1o.d	⊢ 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
2		clwwlkf1o.f	⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝑡 prefix 𝑁 ) )
3	1 2	clwwlkf1	⊢ ( 𝑁 ∈ ℕ → 𝐹 : 𝐷 –1-1→ ( 𝑁 ClWWalksN 𝐺 ) )
4	1 2	clwwlkfo	⊢ ( 𝑁 ∈ ℕ → 𝐹 : 𝐷 –onto→ ( 𝑁 ClWWalksN 𝐺 ) )
5		df-f1o	⊢ ( 𝐹 : 𝐷 –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝐹 : 𝐷 –1-1→ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝐹 : 𝐷 –onto→ ( 𝑁 ClWWalksN 𝐺 ) ) )
6	3 4 5	sylanbrc	⊢ ( 𝑁 ∈ ℕ → 𝐹 : 𝐷 –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) )