Metamath Proof Explorer

Theorem wlklnwwlkn

Description: A walk of length N as word corresponds to a walk with length N in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 12-Apr-2021)

		Ref	Expression
	Assertion	wlklnwwlkn	$⊢ G \in USHGraph \to (\exists f (f Walks (G) P \land \|f\| = N) \leftrightarrow P \in (N WWalksN G))$

Proof

Step	Hyp	Ref	Expression
1		uspgrupgr	$⊢ G \in USHGraph \to G \in UPGraph$
2		wlklnwwlkln1	$⊢ G \in UPGraph \to ((f Walks (G) P \land \|f\| = N) \to P \in (N WWalksN G))$
3	1 2	syl	$⊢ G \in USHGraph \to ((f Walks (G) P \land \|f\| = N) \to P \in (N WWalksN G))$
4	3	exlimdv	$⊢ G \in USHGraph \to (\exists f (f Walks (G) P \land \|f\| = N) \to P \in (N WWalksN G))$
5		wlklnwwlkln2	$⊢ G \in USHGraph \to (P \in (N WWalksN G) \to \exists f (f Walks (G) P \land \|f\| = N))$
6	4 5	impbid	$⊢ G \in USHGraph \to (\exists f (f Walks (G) P \land \|f\| = N) \leftrightarrow P \in (N WWalksN G))$