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

Metamath Proof Explorer

Theorem wlklnwwlknupgr

Description: A walk of length N as word corresponds to a walk with length N in a pseudograph. This variant of wlklnwwlkn does not require G to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice for its proof. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 12-Apr-2021)

Ref Expression
Assertion wlklnwwlknupgr ⊢ G ∈ UPGraph → ∃ f f Walks ⁡ G P ∧ f = N ↔ P ∈ N WWalksN G

Proof

Step Hyp Ref Expression
1 wlklnwwlkln1 ⊢ G ∈ UPGraph → f Walks ⁡ G P ∧ f = N → P ∈ N WWalksN G
2 1 exlimdv ⊢ G ∈ UPGraph → ∃ f f Walks ⁡ G P ∧ f = N → P ∈ N WWalksN G
3 wlklnwwlklnupgr2 ⊢ G ∈ UPGraph → P ∈ N WWalksN G → ∃ f f Walks ⁡ G P ∧ f = N
4 2 3 impbid ⊢ G ∈ UPGraph → ∃ f f Walks ⁡ G P ∧ f = N ↔ P ∈ N WWalksN G