Metamath Proof Explorer

Theorem wlkiswwlkupgr

Description: A walk as word corresponds to a walk in a pseudograph. This variant of wlkiswwlks 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, 10-Apr-2021)

Ref Expression
Assertion wlkiswwlkupgr ⊢ G ∈ UPGraph → ∃ f f Walks ⁡ G P ↔ P ∈ WWalks ⁡ G

Proof

Step Hyp Ref Expression
1 wlkiswwlks1 ⊢ G ∈ UPGraph → f Walks ⁡ G P → P ∈ WWalks ⁡ G
2 1 exlimdv ⊢ G ∈ UPGraph → ∃ f f Walks ⁡ G P → P ∈ WWalks ⁡ G
3 wlkiswwlksupgr2 ⊢ G ∈ UPGraph → P ∈ WWalks ⁡ G → ∃ f f Walks ⁡ G P
4 2 3 impbid ⊢ G ∈ UPGraph → ∃ f f Walks ⁡ G P ↔ P ∈ WWalks ⁡ G