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