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

Metamath Proof Explorer

Theorem wlklnwwlkn

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

Ref Expression
Assertion wlklnwwlkn ( 𝐺 ∈ USPGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ↔ 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 uspgrupgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
2 wlklnwwlkln1 ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) → 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
3 1 2 syl ⊢ ( 𝐺 ∈ USPGraph → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) → 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
4 3 exlimdv ⊢ ( 𝐺 ∈ USPGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) → 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
5 wlklnwwlkln2 ⊢ ( 𝐺 ∈ USPGraph → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) )
6 4 5 impbid ⊢ ( 𝐺 ∈ USPGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ↔ 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ) )