Description: There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018) (Revised by AV, 5-Mar-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wlk0prc | |- ( ( S e/ _V /\ ( Vtx ` S ) = ( Vtx ` G ) ) -> ( Walks ` G ) = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqcom | |- ( ( Vtx ` S ) = ( Vtx ` G ) <-> ( Vtx ` G ) = ( Vtx ` S ) ) |
|
| 2 | 1 | biimpi | |- ( ( Vtx ` S ) = ( Vtx ` G ) -> ( Vtx ` G ) = ( Vtx ` S ) ) |
| 3 | vtxvalprc | |- ( S e/ _V -> ( Vtx ` S ) = (/) ) |
|
| 4 | 2 3 | sylan9eqr | |- ( ( S e/ _V /\ ( Vtx ` S ) = ( Vtx ` G ) ) -> ( Vtx ` G ) = (/) ) |
| 5 | g0wlk0 | |- ( ( Vtx ` G ) = (/) -> ( Walks ` G ) = (/) ) |
|
| 6 | 4 5 | syl | |- ( ( S e/ _V /\ ( Vtx ` S ) = ( Vtx ` G ) ) -> ( Walks ` G ) = (/) ) |