Theorem wlklnwwlknupgr

Description: A walk of length N as word corresponds to a walk with length N in a pseudograph. This variant of wlklnwwlkn 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\in \mathrm{UPGraph}\to \left(\exists f\left(f\mathrm{Walks}\left(G\right)P\wedge \left|f\right|=N\right)\leftrightarrow P\in \left(N\mathrm{WWalksN}G\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		wlklnwwlkln1	$$⊢G\in \mathrm{UPGraph}\to \left(\left(f\mathrm{Walks}\left(G\right)P\wedge \left|f\right|=N\right)\to P\in \left(N\mathrm{WWalksN}G\right)\right)$$
2	1	exlimdv	$$⊢G\in \mathrm{UPGraph}\to \left(\exists f\left(f\mathrm{Walks}\left(G\right)P\wedge \left|f\right|=N\right)\to P\in \left(N\mathrm{WWalksN}G\right)\right)$$
3		wlklnwwlklnupgr2	$$⊢G\in \mathrm{UPGraph}\to \left(P\in \left(N\mathrm{WWalksN}G\right)\to \exists f\left(f\mathrm{Walks}\left(G\right)P\wedge \left|f\right|=N\right)\right)$$
4	2 3	impbid	$$⊢G\in \mathrm{UPGraph}\to \left(\exists f\left(f\mathrm{Walks}\left(G\right)P\wedge \left|f\right|=N\right)\leftrightarrow P\in \left(N\mathrm{WWalksN}G\right)\right)$$