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→∃ffWalks⁡GP↔P∈WWalks⁡G

Proof

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