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 \in Walks (G) \to \exists f \exists p f Walks (G) p$

Step	Hyp	Ref	Expression
1		wlkcpr	$⊢ W \in Walks (G) \leftrightarrow 1^{st} (W) Walks (G) 2^{nd} (W)$
2		fvex	$⊢ 1^{st} (W) \in V$
3		fvex	$⊢ 2^{nd} (W) \in V$
4		breq12	$⊢ (f = 1^{st} (W) \land p = 2^{nd} (W)) \to (f Walks (G) p \leftrightarrow 1^{st} (W) Walks (G) 2^{nd} (W))$
5	2 3 4	spc2ev	$⊢ 1^{st} (W) Walks (G) 2^{nd} (W) \to \exists f \exists p f Walks (G) p$
6	1 5	sylbi	$⊢ W \in Walks (G) \to \exists f \exists p f Walks (G) p$

Metamath Proof Explorer