Description: There is no walk for the empty set, i.e. in a null graph. (Contributed by Alexander van der Vekens, 2-Sep-2018) (Revised by AV, 5-Mar-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0wlk0 | |- ( Walks ` (/) ) = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vtxval0 | |- ( Vtx ` (/) ) = (/) |
|
| 2 | g0wlk0 | |- ( ( Vtx ` (/) ) = (/) -> ( Walks ` (/) ) = (/) ) |
|
| 3 | 1 2 | ax-mp | |- ( Walks ` (/) ) = (/) |