Metamath Proof Explorer


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