This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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