Description: The set of walks as words and the set of (ordinary) walks are equinumerous in a simple pseudograph. (Contributed by AV, 6-May-2021) (Revised by AV, 5-Aug-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wlkswwlksen | |- ( G e. USPGraph -> ( Walks ` G ) ~~ ( WWalks ` G ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | |- ( w e. ( Walks ` G ) |-> ( 2nd ` w ) ) = ( w e. ( Walks ` G ) |-> ( 2nd ` w ) ) |
|
| 2 | 1 | wlkswwlksf1o | |- ( G e. USPGraph -> ( w e. ( Walks ` G ) |-> ( 2nd ` w ) ) : ( Walks ` G ) -1-1-onto-> ( WWalks ` G ) ) |
| 3 | fvex | |- ( Walks ` G ) e. _V |
|
| 4 | 3 | f1oen | |- ( ( w e. ( Walks ` G ) |-> ( 2nd ` w ) ) : ( Walks ` G ) -1-1-onto-> ( WWalks ` G ) -> ( Walks ` G ) ~~ ( WWalks ` G ) ) |
| 5 | 2 4 | syl | |- ( G e. USPGraph -> ( Walks ` G ) ~~ ( WWalks ` G ) ) |