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 D=wNWWalksNG|lastSw=w0
clwwlkf1o.f F=tDtprefixN
Assertion clwwlkf1o NF:D1-1 ontoNClWWalksNG

Proof

Step Hyp Ref Expression
1 clwwlkf1o.d D=wNWWalksNG|lastSw=w0
2 clwwlkf1o.f F=tDtprefixN
3 1 2 clwwlkf1 NF:D1-1NClWWalksNG
4 1 2 clwwlkfo NF:DontoNClWWalksNG
5 df-f1o F:D1-1 ontoNClWWalksNGF:D1-1NClWWalksNGF:DontoNClWWalksNG
6 3 4 5 sylanbrc NF:D1-1 ontoNClWWalksNG