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

Metamath Proof Explorer

Theorem wlklnwwlkln2

Description: A walk of length N as word corresponds to the sequence of vertices in a walk of length N in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 12-Apr-2021)

		Ref	Expression
	Assertion	wlklnwwlkln2	$⊢ G \in USHGraph \to (P \in (N WWalksN G) \to \exists f (f Walks (G) P \land \|f\| = N))$

Proof

Step	Hyp	Ref	Expression
1		wlkiswwlks2	$⊢ G \in USHGraph \to (P \in WWalks (G) \to \exists f f Walks (G) P)$
2	1	wlklnwwlkln2lem	$⊢ G \in USHGraph \to (P \in (N WWalksN G) \to \exists f (f Walks (G) P \land \|f\| = N))$