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	⊢ ( 𝐺 ∈ USPGraph → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		wlkiswwlks2	⊢ ( 𝐺 ∈ USPGraph → ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) )
2	1	wlklnwwlkln2lem	⊢ ( 𝐺 ∈ USPGraph → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) )