Metamath Proof Explorer


Theorem wlkpvtx

Description: A walk connects vertices. (Contributed by AV, 22-Feb-2021)

Ref Expression
Hypothesis wlkpvtx.v V=VtxG
Assertion wlkpvtx FWalksGPN0FPNV

Proof

Step Hyp Ref Expression
1 wlkpvtx.v V=VtxG
2 1 wlkp FWalksGPP:0FV
3 ffvelrn P:0FVN0FPNV
4 3 ex P:0FVN0FPNV
5 2 4 syl FWalksGPN0FPNV