Metamath Proof Explorer


Theorem wlk2f

Description: If there is a walk W there is a pair of functions representing this walk. (Contributed by Alexander van der Vekens, 22-Jul-2018)

Ref Expression
Assertion wlk2f W Walks G f p f Walks G p

Proof

Step Hyp Ref Expression
1 wlkcpr W Walks G 1 st W Walks G 2 nd W
2 fvex 1 st W V
3 fvex 2 nd W V
4 breq12 f = 1 st W p = 2 nd W f Walks G p 1 st W Walks G 2 nd W
5 2 3 4 spc2ev 1 st W Walks G 2 nd W f p f Walks G p
6 1 5 sylbi W Walks G f p f Walks G p