Metamath Proof Explorer


Theorem wlklnwwlklnupgr2

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

Ref Expression
Assertion wlklnwwlklnupgr2
|- ( G e. UPGraph -> ( P e. ( N WWalksN G ) -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) )

Proof

Step Hyp Ref Expression
1 wlkiswwlksupgr2
 |-  ( G e. UPGraph -> ( P e. ( WWalks ` G ) -> E. f f ( Walks ` G ) P ) )
2 1 wlklnwwlkln2lem
 |-  ( G e. UPGraph -> ( P e. ( N WWalksN G ) -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) )