Description: A walk as word corresponds to a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 10-Apr-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wlkiswwlks | |- ( G e. USPGraph -> ( E. f f ( Walks ` G ) P <-> P e. ( WWalks ` G ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uspgrupgr | |- ( G e. USPGraph -> G e. UPGraph ) |
|
| 2 | wlkiswwlks1 | |- ( G e. UPGraph -> ( f ( Walks ` G ) P -> P e. ( WWalks ` G ) ) ) |
|
| 3 | 1 2 | syl | |- ( G e. USPGraph -> ( f ( Walks ` G ) P -> P e. ( WWalks ` G ) ) ) |
| 4 | 3 | exlimdv | |- ( G e. USPGraph -> ( E. f f ( Walks ` G ) P -> P e. ( WWalks ` G ) ) ) |
| 5 | wlkiswwlks2 | |- ( G e. USPGraph -> ( P e. ( WWalks ` G ) -> E. f f ( Walks ` G ) P ) ) |
|
| 6 | 4 5 | impbid | |- ( G e. USPGraph -> ( E. f f ( Walks ` G ) P <-> P e. ( WWalks ` G ) ) ) |