Metamath Proof Explorer


Theorem wwlksnon0

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=VtxG
Assertion wwlksnon0 ¬N0GVAVBVANWWalksNOnGB=

Proof

Step Hyp Ref Expression
1 wwlksnon0.v V=VtxG
2 df-wwlksnon WWalksNOn=n0,gVaVtxg,bVtxgwnWWalksNg|w0=awn=b
3 1 wwlksnon N0GVNWWalksNOnG=aV,bVwNWWalksNG|w0=awN=b
4 2 3 2mpo0 ¬N0GVAVBVANWWalksNOnGB=