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 e. USPGraph -> ( E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) <-> P e. ( N WWalksN G ) ) )

Proof

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