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