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∈NWWalksNG→∀i∈0…NW⁡i∈Vtx⁡G

Proof

Step Hyp Ref Expression
1 wwlknbp1 ⊢W∈NWWalksNG→N∈ℕ0∧W∈WordVtx⁡G∧W=N+1
2 simp2 ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1→W∈WordVtx⁡G
3 nn0z ⊢N∈ℕ0→N∈ℤ
4 fzval3 ⊢N∈ℤ→0…N=0..^N+1
5 3 4 syl ⊢N∈ℕ0→0…N=0..^N+1
6 5 3ad2ant1 ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1→0…N=0..^N+1
7 6 eleq2d ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1→i∈0…N↔i∈0..^N+1
8 7 biimpa ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1∧i∈0…N→i∈0..^N+1
9 oveq2 ⊢W=N+1→0..^W=0..^N+1
10 9 eleq2d ⊢W=N+1→i∈0..^W↔i∈0..^N+1
11 10 3ad2ant3 ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1→i∈0..^W↔i∈0..^N+1
12 11 adantr ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1∧i∈0…N→i∈0..^W↔i∈0..^N+1
13 8 12 mpbird ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1∧i∈0…N→i∈0..^W
14 wrdsymbcl ⊢W∈WordVtx⁡G∧i∈0..^W→W⁡i∈Vtx⁡G
15 2 13 14 syl2an2r ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1∧i∈0…N→W⁡i∈Vtx⁡G
16 15 ralrimiva ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1→∀i∈0…NW⁡i∈Vtx⁡G
17 1 16 syl ⊢W∈NWWalksNG→∀i∈0…NW⁡i∈Vtx⁡G