Metamath Proof Explorer

Theorem redwlk

Description: A walk ending at the last but one vertex of the walk is a walk. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 29-Jan-2021)

Ref Expression
Assertion redwlk ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ( Walks ‘ 𝐺 ) ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 wlkv ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
4 2 3 iswlk ⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
5 wrdred1 ⊢ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word dom ( iEdg ‘ 𝐺 ) )
6 5 a1i ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word dom ( iEdg ‘ 𝐺 ) ) )
7 3 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )
8 redwlklem ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) )
9 8 3exp ⊢ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( 1 ≤ ( ♯ ‘ 𝐹 ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) )
10 7 9 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 1 ≤ ( ♯ ‘ 𝐹 ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) )
11 10 imp ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
12 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
13 wrdred1hash ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐹 ) − 1 ) )
14 7 13 sylan ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐹 ) − 1 ) )
15 nn0z ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℤ )
16 fzossrbm1 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℤ → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
17 15 16 syl ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
18 ssralv ⊢ ( ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
19 17 18 syl ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
20 17 sselda ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
21 20 fvresd ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) )
22 21 eqcomd ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( 𝑃 ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) )
23 fzo0ss1 ⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
24 simpr ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
25 15 adantr ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ℤ )
26 1zzd ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → 1 ∈ ℤ )
27 fzoaddel2 ⊢ ( ( 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑘 + 1 ) ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
28 24 25 26 27 syl3anc ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
29 23 28 sselid ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
30 29 fvresd ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
31 30 eqcomd ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) )
32 22 31 eqeq12d ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
33 fvres ⊢ ( 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
34 33 adantl ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
35 34 eqcomd ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) )
36 35 fveq2d ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) )
37 22 sneqd ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → { ( 𝑃 ‘ 𝑘 ) } = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } )
38 36 37 eqeq12d ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } ) )
39 22 31 preq12d ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } )
40 39 36 sseq12d ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) )
41 32 38 40 ifpbi123d ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) )
42 41 biimpd ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) )
43 42 ralimdva ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) )
44 19 43 syld ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) )
45 44 adantr ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) )
46 oveq2 ⊢ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
47 46 eqcomd ⊢ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) = ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) )
48 47 raleqdv ⊢ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ↔ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) )
49 48 adantl ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ↔ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) )
50 45 49 sylibd ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) )
51 12 14 50 syl2an2r ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) )
52 6 11 51 3anim123d ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) ) )
53 52 imp ⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) → ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) )
54 id ⊢ ( 𝐺 ∈ V → 𝐺 ∈ V )
55 resexg ⊢ ( 𝐹 ∈ V → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ V )
56 resexg ⊢ ( 𝑃 ∈ V → ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∈ V )
57 2 3 iswlk ⊢ ( ( 𝐺 ∈ V ∧ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ V ∧ ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∈ V ) → ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ( Walks ‘ 𝐺 ) ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) ) )
58 57 bicomd ⊢ ( ( 𝐺 ∈ V ∧ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ V ∧ ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∈ V ) → ( ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) ↔ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ( Walks ‘ 𝐺 ) ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
59 54 55 56 58 syl3an ⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) if- ( ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) = ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) = { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) } , { ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝑘 ) , ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ‘ 𝑘 ) ) ) ) ↔ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ( Walks ‘ 𝐺 ) ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
60 53 59 imbitrid ⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ( Walks ‘ 𝐺 ) ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
61 60 expcomd ⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ( Walks ‘ 𝐺 ) ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) )
62 4 61 sylbid ⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ( Walks ‘ 𝐺 ) ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) )
63 1 62 mpcom ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ( Walks ‘ 𝐺 ) ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
64 63 anabsi5 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ( Walks ‘ 𝐺 ) ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )