Metamath Proof Explorer

Theorem wwlknbp1

Description: Other basic properties of a walk of a fixed length as word. (Contributed by AV, 8-Mar-2022)

Ref Expression
Assertion wwlknbp1 
|- ( W e. ( N WWalksN G ) -> ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 wwlknbp 
 |-  ( W e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ W e. Word ( Vtx ` G ) ) )
3 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
4 1 3 wwlknp 
 |-  ( W e. ( N WWalksN G ) -> ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
5 simpl 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> N e. NN0 )
6 simpr1 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> W e. Word ( Vtx ` G ) )
7 simpr2 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> ( # ` W ) = ( N + 1 ) )
8 5 6 7 3jca 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) -> ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) )
9 8 ex 
 |-  ( N e. NN0 -> ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) )
10 9 3ad2ant2 
 |-  ( ( G e. _V /\ N e. NN0 /\ W e. Word ( Vtx ` G ) ) -> ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) )
11 2 4 10 sylc 
 |-  ( W e. ( N WWalksN G ) -> ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) )