Metamath Proof Explorer

Theorem wlkiswwlks

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

Ref Expression
Assertion wlkiswwlks ⊢ G ∈ USHGraph → ∃ f f Walks ⁡ G P ↔ P ∈ WWalks ⁡ G

Proof

Step Hyp Ref Expression
1 uspgrupgr ⊢ G ∈ USHGraph → G ∈ UPGraph
2 wlkiswwlks1 ⊢ G ∈ UPGraph → f Walks ⁡ G P → P ∈ WWalks ⁡ G
3 1 2 syl ⊢ G ∈ USHGraph → f Walks ⁡ G P → P ∈ WWalks ⁡ G
4 3 exlimdv ⊢ G ∈ USHGraph → ∃ f f Walks ⁡ G P → P ∈ WWalks ⁡ G
5 wlkiswwlks2 ⊢ G ∈ USHGraph → P ∈ WWalks ⁡ G → ∃ f f Walks ⁡ G P
6 4 5 impbid ⊢ G ∈ USHGraph → ∃ f f Walks ⁡ G P ↔ P ∈ WWalks ⁡ G