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 ) )