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	⊢ ( 𝐺 ∈ UPGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ↔ 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		wlklnwwlkln1	⊢ ( 𝐺 ∈ UPGraph → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) → 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
2	1	exlimdv	⊢ ( 𝐺 ∈ UPGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) → 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
3		wlklnwwlklnupgr2	⊢ ( 𝐺 ∈ UPGraph → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) )
4	2 3	impbid	⊢ ( 𝐺 ∈ UPGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ↔ 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ) )

Metamath Proof Explorer

Theorem wlklnwwlknupgr

Proof