Description: Sufficient conditions for a set of walks of a fixed length between two vertices to be empty. (Contributed by AV, 15-May-2021) (Proof shortened by AV, 21-May-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | wwlksnon0.v | |- V = ( Vtx ` G ) |
|
| Assertion | wwlksnon0 | |- ( -. ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( A ( N WWalksNOn G ) B ) = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wwlksnon0.v | |- V = ( Vtx ` G ) |
|
| 2 | df-wwlksnon | |- WWalksNOn = ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } ) ) |
|
| 3 | 1 | wwlksnon | |- ( ( N e. NN0 /\ G e. _V ) -> ( N WWalksNOn G ) = ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) ) |
| 4 | 2 3 | 2mpo0 | |- ( -. ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( A ( N WWalksNOn G ) B ) = (/) ) |