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	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )

Proof

Step	Hyp	Ref	Expression
1		wlkcpr	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑊 ) )
2		fvex	⊢ ( 1st ‘ 𝑊 ) ∈ V
3		fvex	⊢ ( 2nd ‘ 𝑊 ) ∈ V
4		breq12	⊢ ( ( 𝑓 = ( 1st ‘ 𝑊 ) ∧ 𝑝 = ( 2nd ‘ 𝑊 ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ↔ ( 1st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑊 ) ) )
5	2 3 4	spc2ev	⊢ ( ( 1st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑊 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
6	1 5	sylbi	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )