Metamath Proof Explorer


Theorem clwlkclwwlkf1o

Description: F is a bijection between the nonempty closed walks and the closed walks as words in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018) (Revised by AV, 3-May-2021) (Revised by AV, 29-Oct-2022)

Ref Expression
Hypotheses clwlkclwwlkf.c
|- C = { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) }
clwlkclwwlkf.f
|- F = ( c e. C |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) )
Assertion clwlkclwwlkf1o
|- ( G e. USPGraph -> F : C -1-1-onto-> ( ClWWalks ` G ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c
 |-  C = { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) }
2 clwlkclwwlkf.f
 |-  F = ( c e. C |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) )
3 1 2 clwlkclwwlkf1
 |-  ( G e. USPGraph -> F : C -1-1-> ( ClWWalks ` G ) )
4 1 2 clwlkclwwlkfo
 |-  ( G e. USPGraph -> F : C -onto-> ( ClWWalks ` G ) )
5 df-f1o
 |-  ( F : C -1-1-onto-> ( ClWWalks ` G ) <-> ( F : C -1-1-> ( ClWWalks ` G ) /\ F : C -onto-> ( ClWWalks ` G ) ) )
6 3 4 5 sylanbrc
 |-  ( G e. USPGraph -> F : C -1-1-onto-> ( ClWWalks ` G ) )