Theorem wlklnwwlknupgr

Description: A walk of length N as word corresponds to a walk with length N 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, 12-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		wlklnwwlkln1	|- ( G e. UPGraph -> ( ( f ( Walks ` G ) P /\ ( # ` f ) = N ) -> P e. ( N WWalksN G ) ) )
2	1	exlimdv	|- ( G e. UPGraph -> ( E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) -> P e. ( N WWalksN G ) ) )
3		wlklnwwlklnupgr2	|- ( G e. UPGraph -> ( P e. ( N WWalksN G ) -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) )
4	2 3	impbid	|- ( G e. UPGraph -> ( E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) <-> P e. ( N WWalksN G ) ) )