Metamath Proof Explorer

Theorem wlk1ewlk

Description: A walk is an s-walk "on the edge level" (with s=1) according to Aksoy et al. (Contributed by AV, 5-Jan-2021)

Ref Expression
Assertion wlk1ewlk 
|- ( F ( Walks ` G ) P -> F e. ( G EdgWalks 1 ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
2 1 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom ( iEdg ` G ) )
3 1 wlk1walk 
 |-  ( F ( Walks ` G ) P -> A. k e. ( 1 ..^ ( # ` F ) ) 1 <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
4 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
5 4 simp1d 
 |-  ( F ( Walks ` G ) P -> G e. _V )
6 1nn0 
 |-  1 e. NN0
7 nn0xnn0 
 |-  ( 1 e. NN0 -> 1 e. NN0* )
8 6 7 mp1i 
 |-  ( F ( Walks ` G ) P -> 1 e. NN0* )
9 1 isewlk 
 |-  ( ( G e. _V /\ 1 e. NN0* /\ F e. Word dom ( iEdg ` G ) ) -> ( F e. ( G EdgWalks 1 ) <-> ( F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) 1 <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) ) )
10 5 8 2 9 syl3anc 
 |-  ( F ( Walks ` G ) P -> ( F e. ( G EdgWalks 1 ) <-> ( F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) 1 <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) ) )
11 2 3 10 mpbir2and 
 |-  ( F ( Walks ` G ) P -> F e. ( G EdgWalks 1 ) )