Metamath Proof Explorer

Theorem wwlknvtx

Description: The symbols of a word W representing a walk of a fixed length N are vertices. (Contributed by AV, 16-Mar-2022)

Ref Expression
Assertion wwlknvtx 
|- ( W e. ( N WWalksN G ) -> A. i e. ( 0 ... N ) ( W ` i ) e. ( Vtx ` G ) )

Proof

Step Hyp Ref Expression
1 wwlknbp1 
 |-  ( W e. ( N WWalksN G ) -> ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) )
2 simp2 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> W e. Word ( Vtx ` G ) )
3 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
4 fzval3 
 |-  ( N e. ZZ -> ( 0 ... N ) = ( 0 ..^ ( N + 1 ) ) )
5 3 4 syl 
 |-  ( N e. NN0 -> ( 0 ... N ) = ( 0 ..^ ( N + 1 ) ) )
6 5 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( 0 ... N ) = ( 0 ..^ ( N + 1 ) ) )
7 6 eleq2d 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( i e. ( 0 ... N ) <-> i e. ( 0 ..^ ( N + 1 ) ) ) )
8 7 biimpa 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ i e. ( 0 ... N ) ) -> i e. ( 0 ..^ ( N + 1 ) ) )
9 oveq2 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ ( N + 1 ) ) )
10 9 eleq2d 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( i e. ( 0 ..^ ( # ` W ) ) <-> i e. ( 0 ..^ ( N + 1 ) ) ) )
11 10 3ad2ant3 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ ( # ` W ) ) <-> i e. ( 0 ..^ ( N + 1 ) ) ) )
12 11 adantr 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ i e. ( 0 ... N ) ) -> ( i e. ( 0 ..^ ( # ` W ) ) <-> i e. ( 0 ..^ ( N + 1 ) ) ) )
13 8 12 mpbird 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ i e. ( 0 ... N ) ) -> i e. ( 0 ..^ ( # ` W ) ) )
14 wrdsymbcl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` i ) e. ( Vtx ` G ) )
15 2 13 14 syl2an2r 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ i e. ( 0 ... N ) ) -> ( W ` i ) e. ( Vtx ` G ) )
16 15 ralrimiva 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> A. i e. ( 0 ... N ) ( W ` i ) e. ( Vtx ` G ) )
17 1 16 syl 
 |-  ( W e. ( N WWalksN G ) -> A. i e. ( 0 ... N ) ( W ` i ) e. ( Vtx ` G ) )