Metamath Proof Explorer


Theorem pfxwlk

Description: A prefix of a walk is a walk. (Contributed by BTernaryTau, 2-Dec-2023)

Ref Expression
Assertion pfxwlk ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 𝐹 prefix 𝐿 ) ( Walks β€˜ 𝐺 ) ( 𝑃 prefix ( 𝐿 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊒ ( iEdg β€˜ 𝐺 ) = ( iEdg β€˜ 𝐺 )
2 1 wlkf ⊒ ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 β†’ 𝐹 ∈ Word dom ( iEdg β€˜ 𝐺 ) )
3 2 adantr ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ 𝐹 ∈ Word dom ( iEdg β€˜ 𝐺 ) )
4 pfxcl ⊒ ( 𝐹 ∈ Word dom ( iEdg β€˜ 𝐺 ) β†’ ( 𝐹 prefix 𝐿 ) ∈ Word dom ( iEdg β€˜ 𝐺 ) )
5 3 4 syl ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 𝐹 prefix 𝐿 ) ∈ Word dom ( iEdg β€˜ 𝐺 ) )
6 eqid ⊒ ( Vtx β€˜ 𝐺 ) = ( Vtx β€˜ 𝐺 )
7 6 wlkp ⊒ ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 β†’ 𝑃 : ( 0 ... ( β™― β€˜ 𝐹 ) ) ⟢ ( Vtx β€˜ 𝐺 ) )
8 7 adantr ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ 𝑃 : ( 0 ... ( β™― β€˜ 𝐹 ) ) ⟢ ( Vtx β€˜ 𝐺 ) )
9 elfzuz3 ⊒ ( 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) β†’ ( β™― β€˜ 𝐹 ) ∈ ( β„€β‰₯ β€˜ 𝐿 ) )
10 fzss2 ⊒ ( ( β™― β€˜ 𝐹 ) ∈ ( β„€β‰₯ β€˜ 𝐿 ) β†’ ( 0 ... 𝐿 ) βŠ† ( 0 ... ( β™― β€˜ 𝐹 ) ) )
11 9 10 syl ⊒ ( 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) β†’ ( 0 ... 𝐿 ) βŠ† ( 0 ... ( β™― β€˜ 𝐹 ) ) )
12 11 adantl ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 0 ... 𝐿 ) βŠ† ( 0 ... ( β™― β€˜ 𝐹 ) ) )
13 8 12 fssresd ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 𝑃 β†Ύ ( 0 ... 𝐿 ) ) : ( 0 ... 𝐿 ) ⟢ ( Vtx β€˜ 𝐺 ) )
14 pfxlen ⊒ ( ( 𝐹 ∈ Word dom ( iEdg β€˜ 𝐺 ) ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) = 𝐿 )
15 2 14 sylan ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) = 𝐿 )
16 15 oveq2d ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 0 ... ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) = ( 0 ... 𝐿 ) )
17 16 feq2d ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( ( 𝑃 β†Ύ ( 0 ... 𝐿 ) ) : ( 0 ... ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ⟢ ( Vtx β€˜ 𝐺 ) ↔ ( 𝑃 β†Ύ ( 0 ... 𝐿 ) ) : ( 0 ... 𝐿 ) ⟢ ( Vtx β€˜ 𝐺 ) ) )
18 13 17 mpbird ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 𝑃 β†Ύ ( 0 ... 𝐿 ) ) : ( 0 ... ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ⟢ ( Vtx β€˜ 𝐺 ) )
19 6 wlkpwrd ⊒ ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 β†’ 𝑃 ∈ Word ( Vtx β€˜ 𝐺 ) )
20 fzp1elp1 ⊒ ( 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) β†’ ( 𝐿 + 1 ) ∈ ( 0 ... ( ( β™― β€˜ 𝐹 ) + 1 ) ) )
21 20 adantl ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 𝐿 + 1 ) ∈ ( 0 ... ( ( β™― β€˜ 𝐹 ) + 1 ) ) )
22 wlklenvp1 ⊒ ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 β†’ ( β™― β€˜ 𝑃 ) = ( ( β™― β€˜ 𝐹 ) + 1 ) )
23 22 oveq2d ⊒ ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 β†’ ( 0 ... ( β™― β€˜ 𝑃 ) ) = ( 0 ... ( ( β™― β€˜ 𝐹 ) + 1 ) ) )
24 23 adantr ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 0 ... ( β™― β€˜ 𝑃 ) ) = ( 0 ... ( ( β™― β€˜ 𝐹 ) + 1 ) ) )
25 21 24 eleqtrrd ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 𝐿 + 1 ) ∈ ( 0 ... ( β™― β€˜ 𝑃 ) ) )
26 pfxres ⊒ ( ( 𝑃 ∈ Word ( Vtx β€˜ 𝐺 ) ∧ ( 𝐿 + 1 ) ∈ ( 0 ... ( β™― β€˜ 𝑃 ) ) ) β†’ ( 𝑃 prefix ( 𝐿 + 1 ) ) = ( 𝑃 β†Ύ ( 0 ..^ ( 𝐿 + 1 ) ) ) )
27 19 25 26 syl2an2r ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 𝑃 prefix ( 𝐿 + 1 ) ) = ( 𝑃 β†Ύ ( 0 ..^ ( 𝐿 + 1 ) ) ) )
28 elfzelz ⊒ ( 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) β†’ 𝐿 ∈ β„€ )
29 fzval3 ⊒ ( 𝐿 ∈ β„€ β†’ ( 0 ... 𝐿 ) = ( 0 ..^ ( 𝐿 + 1 ) ) )
30 28 29 syl ⊒ ( 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) β†’ ( 0 ... 𝐿 ) = ( 0 ..^ ( 𝐿 + 1 ) ) )
31 30 adantl ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 0 ... 𝐿 ) = ( 0 ..^ ( 𝐿 + 1 ) ) )
32 31 reseq2d ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 𝑃 β†Ύ ( 0 ... 𝐿 ) ) = ( 𝑃 β†Ύ ( 0 ..^ ( 𝐿 + 1 ) ) ) )
33 27 32 eqtr4d ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 𝑃 prefix ( 𝐿 + 1 ) ) = ( 𝑃 β†Ύ ( 0 ... 𝐿 ) ) )
34 33 feq1d ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( ( 𝑃 prefix ( 𝐿 + 1 ) ) : ( 0 ... ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ⟢ ( Vtx β€˜ 𝐺 ) ↔ ( 𝑃 β†Ύ ( 0 ... 𝐿 ) ) : ( 0 ... ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ⟢ ( Vtx β€˜ 𝐺 ) ) )
35 18 34 mpbird ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 𝑃 prefix ( 𝐿 + 1 ) ) : ( 0 ... ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ⟢ ( Vtx β€˜ 𝐺 ) )
36 6 1 wlkprop ⊒ ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 β†’ ( 𝐹 ∈ Word dom ( iEdg β€˜ 𝐺 ) ∧ 𝑃 : ( 0 ... ( β™― β€˜ 𝐹 ) ) ⟢ ( Vtx β€˜ 𝐺 ) ∧ βˆ€ π‘₯ ∈ ( 0 ..^ ( β™― β€˜ 𝐹 ) ) if- ( ( 𝑃 β€˜ π‘₯ ) = ( 𝑃 β€˜ ( π‘₯ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) = { ( 𝑃 β€˜ π‘₯ ) } , { ( 𝑃 β€˜ π‘₯ ) , ( 𝑃 β€˜ ( π‘₯ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) ) ) )
37 36 simp3d ⊒ ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 β†’ βˆ€ π‘₯ ∈ ( 0 ..^ ( β™― β€˜ 𝐹 ) ) if- ( ( 𝑃 β€˜ π‘₯ ) = ( 𝑃 β€˜ ( π‘₯ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) = { ( 𝑃 β€˜ π‘₯ ) } , { ( 𝑃 β€˜ π‘₯ ) , ( 𝑃 β€˜ ( π‘₯ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) ) )
38 37 adantr ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ βˆ€ π‘₯ ∈ ( 0 ..^ ( β™― β€˜ 𝐹 ) ) if- ( ( 𝑃 β€˜ π‘₯ ) = ( 𝑃 β€˜ ( π‘₯ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) = { ( 𝑃 β€˜ π‘₯ ) } , { ( 𝑃 β€˜ π‘₯ ) , ( 𝑃 β€˜ ( π‘₯ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) ) )
39 38 adantr ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ) β†’ βˆ€ π‘₯ ∈ ( 0 ..^ ( β™― β€˜ 𝐹 ) ) if- ( ( 𝑃 β€˜ π‘₯ ) = ( 𝑃 β€˜ ( π‘₯ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) = { ( 𝑃 β€˜ π‘₯ ) } , { ( 𝑃 β€˜ π‘₯ ) , ( 𝑃 β€˜ ( π‘₯ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) ) )
40 15 oveq2d ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) = ( 0 ..^ 𝐿 ) )
41 40 eleq2d ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ↔ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) )
42 33 fveq1d ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) = ( ( 𝑃 β†Ύ ( 0 ... 𝐿 ) ) β€˜ π‘˜ ) )
43 42 adantr ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) = ( ( 𝑃 β†Ύ ( 0 ... 𝐿 ) ) β€˜ π‘˜ ) )
44 fzossfz ⊒ ( 0 ..^ 𝐿 ) βŠ† ( 0 ... 𝐿 )
45 44 a1i ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 0 ..^ 𝐿 ) βŠ† ( 0 ... 𝐿 ) )
46 45 sselda ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ π‘˜ ∈ ( 0 ... 𝐿 ) )
47 46 fvresd ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ ( ( 𝑃 β†Ύ ( 0 ... 𝐿 ) ) β€˜ π‘˜ ) = ( 𝑃 β€˜ π‘˜ ) )
48 43 47 eqtr2d ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) )
49 33 fveq1d ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 β†Ύ ( 0 ... 𝐿 ) ) β€˜ ( π‘˜ + 1 ) ) )
50 49 adantr ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 β†Ύ ( 0 ... 𝐿 ) ) β€˜ ( π‘˜ + 1 ) ) )
51 fzofzp1 ⊒ ( π‘˜ ∈ ( 0 ..^ 𝐿 ) β†’ ( π‘˜ + 1 ) ∈ ( 0 ... 𝐿 ) )
52 51 adantl ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ ( π‘˜ + 1 ) ∈ ( 0 ... 𝐿 ) )
53 52 fvresd ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ ( ( 𝑃 β†Ύ ( 0 ... 𝐿 ) ) β€˜ ( π‘˜ + 1 ) ) = ( 𝑃 β€˜ ( π‘˜ + 1 ) ) )
54 50 53 eqtr2d ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) )
55 48 54 jca ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) )
56 55 ex ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( π‘˜ ∈ ( 0 ..^ 𝐿 ) β†’ ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) ) )
57 41 56 sylbid ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) β†’ ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) ) )
58 57 imp ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ) β†’ ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) )
59 3 ancli ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg β€˜ 𝐺 ) ) )
60 simpr ⊒ ( ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg β€˜ 𝐺 ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ π‘˜ ∈ ( 0 ..^ 𝐿 ) )
61 60 fvresd ⊒ ( ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg β€˜ 𝐺 ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ ( ( 𝐹 β†Ύ ( 0 ..^ 𝐿 ) ) β€˜ π‘˜ ) = ( 𝐹 β€˜ π‘˜ ) )
62 61 fveq2d ⊒ ( ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg β€˜ 𝐺 ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 β†Ύ ( 0 ..^ 𝐿 ) ) β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) )
63 59 62 sylan ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 β†Ύ ( 0 ..^ 𝐿 ) ) β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) )
64 63 eqcomd ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ 𝐿 ) ) β†’ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 β†Ύ ( 0 ..^ 𝐿 ) ) β€˜ π‘˜ ) ) )
65 64 ex ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( π‘˜ ∈ ( 0 ..^ 𝐿 ) β†’ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 β†Ύ ( 0 ..^ 𝐿 ) ) β€˜ π‘˜ ) ) ) )
66 41 65 sylbid ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) β†’ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 β†Ύ ( 0 ..^ 𝐿 ) ) β€˜ π‘˜ ) ) ) )
67 66 imp ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ) β†’ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 β†Ύ ( 0 ..^ 𝐿 ) ) β€˜ π‘˜ ) ) )
68 simplr ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ) β†’ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) )
69 pfxres ⊒ ( ( 𝐹 ∈ Word dom ( iEdg β€˜ 𝐺 ) ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 𝐹 prefix 𝐿 ) = ( 𝐹 β†Ύ ( 0 ..^ 𝐿 ) ) )
70 3 68 69 syl2an2r ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ) β†’ ( 𝐹 prefix 𝐿 ) = ( 𝐹 β†Ύ ( 0 ..^ 𝐿 ) ) )
71 70 fveq1d ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ) β†’ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) = ( ( 𝐹 β†Ύ ( 0 ..^ 𝐿 ) ) β€˜ π‘˜ ) )
72 71 fveq2d ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ) β†’ ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 β†Ύ ( 0 ..^ 𝐿 ) ) β€˜ π‘˜ ) ) )
73 67 72 eqtr4d ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ) β†’ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) )
74 58 73 jca ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ) β†’ ( ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) ∧ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) )
75 9 adantl ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( β™― β€˜ 𝐹 ) ∈ ( β„€β‰₯ β€˜ 𝐿 ) )
76 15 fveq2d ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( β„€β‰₯ β€˜ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) = ( β„€β‰₯ β€˜ 𝐿 ) )
77 75 76 eleqtrrd ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( β™― β€˜ 𝐹 ) ∈ ( β„€β‰₯ β€˜ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) )
78 fzoss2 ⊒ ( ( β™― β€˜ 𝐹 ) ∈ ( β„€β‰₯ β€˜ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) β†’ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) βŠ† ( 0 ..^ ( β™― β€˜ 𝐹 ) ) )
79 77 78 syl ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) βŠ† ( 0 ..^ ( β™― β€˜ 𝐹 ) ) )
80 79 sselda ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ) β†’ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ 𝐹 ) ) )
81 wkslem1 ⊒ ( π‘₯ = π‘˜ β†’ ( if- ( ( 𝑃 β€˜ π‘₯ ) = ( 𝑃 β€˜ ( π‘₯ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) = { ( 𝑃 β€˜ π‘₯ ) } , { ( 𝑃 β€˜ π‘₯ ) , ( 𝑃 β€˜ ( π‘₯ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) ) ↔ if- ( ( 𝑃 β€˜ π‘˜ ) = ( 𝑃 β€˜ ( π‘˜ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = { ( 𝑃 β€˜ π‘˜ ) } , { ( 𝑃 β€˜ π‘˜ ) , ( 𝑃 β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) ) ) )
82 81 rspcv ⊒ ( π‘˜ ∈ ( 0 ..^ ( β™― β€˜ 𝐹 ) ) β†’ ( βˆ€ π‘₯ ∈ ( 0 ..^ ( β™― β€˜ 𝐹 ) ) if- ( ( 𝑃 β€˜ π‘₯ ) = ( 𝑃 β€˜ ( π‘₯ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) = { ( 𝑃 β€˜ π‘₯ ) } , { ( 𝑃 β€˜ π‘₯ ) , ( 𝑃 β€˜ ( π‘₯ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) ) β†’ if- ( ( 𝑃 β€˜ π‘˜ ) = ( 𝑃 β€˜ ( π‘˜ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = { ( 𝑃 β€˜ π‘˜ ) } , { ( 𝑃 β€˜ π‘˜ ) , ( 𝑃 β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) ) ) )
83 80 82 syl ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ) β†’ ( βˆ€ π‘₯ ∈ ( 0 ..^ ( β™― β€˜ 𝐹 ) ) if- ( ( 𝑃 β€˜ π‘₯ ) = ( 𝑃 β€˜ ( π‘₯ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) = { ( 𝑃 β€˜ π‘₯ ) } , { ( 𝑃 β€˜ π‘₯ ) , ( 𝑃 β€˜ ( π‘₯ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) ) β†’ if- ( ( 𝑃 β€˜ π‘˜ ) = ( 𝑃 β€˜ ( π‘˜ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = { ( 𝑃 β€˜ π‘˜ ) } , { ( 𝑃 β€˜ π‘˜ ) , ( 𝑃 β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) ) ) )
84 eqeq12 ⊒ ( ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) β†’ ( ( 𝑃 β€˜ π‘˜ ) = ( 𝑃 β€˜ ( π‘˜ + 1 ) ) ↔ ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) )
85 84 adantr ⊒ ( ( ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) ∧ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) β†’ ( ( 𝑃 β€˜ π‘˜ ) = ( 𝑃 β€˜ ( π‘˜ + 1 ) ) ↔ ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) )
86 simpr ⊒ ( ( ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) ∧ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) β†’ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) )
87 sneq ⊒ ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) β†’ { ( 𝑃 β€˜ π‘˜ ) } = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) } )
88 87 adantr ⊒ ( ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) β†’ { ( 𝑃 β€˜ π‘˜ ) } = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) } )
89 88 adantr ⊒ ( ( ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) ∧ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) β†’ { ( 𝑃 β€˜ π‘˜ ) } = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) } )
90 86 89 eqeq12d ⊒ ( ( ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) ∧ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) β†’ ( ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = { ( 𝑃 β€˜ π‘˜ ) } ↔ ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) } ) )
91 preq12 ⊒ ( ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) β†’ { ( 𝑃 β€˜ π‘˜ ) , ( 𝑃 β€˜ ( π‘˜ + 1 ) ) } = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) } )
92 91 adantr ⊒ ( ( ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) ∧ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) β†’ { ( 𝑃 β€˜ π‘˜ ) , ( 𝑃 β€˜ ( π‘˜ + 1 ) ) } = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) } )
93 92 86 sseq12d ⊒ ( ( ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) ∧ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) β†’ ( { ( 𝑃 β€˜ π‘˜ ) , ( 𝑃 β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) ↔ { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) )
94 85 90 93 ifpbi123d ⊒ ( ( ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) ∧ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) β†’ ( if- ( ( 𝑃 β€˜ π‘˜ ) = ( 𝑃 β€˜ ( π‘˜ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = { ( 𝑃 β€˜ π‘˜ ) } , { ( 𝑃 β€˜ π‘˜ ) , ( 𝑃 β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) ) ↔ if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) ) )
95 94 biimpd ⊒ ( ( ( ( 𝑃 β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) ∧ ( 𝑃 β€˜ ( π‘˜ + 1 ) ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) ) ∧ ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) β†’ ( if- ( ( 𝑃 β€˜ π‘˜ ) = ( 𝑃 β€˜ ( π‘˜ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = { ( 𝑃 β€˜ π‘˜ ) } , { ( 𝑃 β€˜ π‘˜ ) , ( 𝑃 β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) ) β†’ if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) ) )
96 74 83 95 sylsyld ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ) β†’ ( βˆ€ π‘₯ ∈ ( 0 ..^ ( β™― β€˜ 𝐹 ) ) if- ( ( 𝑃 β€˜ π‘₯ ) = ( 𝑃 β€˜ ( π‘₯ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) = { ( 𝑃 β€˜ π‘₯ ) } , { ( 𝑃 β€˜ π‘₯ ) , ( 𝑃 β€˜ ( π‘₯ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( 𝐹 β€˜ π‘₯ ) ) ) β†’ if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) ) )
97 39 96 mpd ⊒ ( ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) ∧ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ) β†’ if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) )
98 97 ralrimiva ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ βˆ€ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) )
99 wlkv ⊒ ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 β†’ ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
100 99 simp1d ⊒ ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 β†’ 𝐺 ∈ V )
101 100 adantr ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ 𝐺 ∈ V )
102 6 1 iswlkg ⊒ ( 𝐺 ∈ V β†’ ( ( 𝐹 prefix 𝐿 ) ( Walks β€˜ 𝐺 ) ( 𝑃 prefix ( 𝐿 + 1 ) ) ↔ ( ( 𝐹 prefix 𝐿 ) ∈ Word dom ( iEdg β€˜ 𝐺 ) ∧ ( 𝑃 prefix ( 𝐿 + 1 ) ) : ( 0 ... ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ⟢ ( Vtx β€˜ 𝐺 ) ∧ βˆ€ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) ) ) )
103 101 102 syl ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( ( 𝐹 prefix 𝐿 ) ( Walks β€˜ 𝐺 ) ( 𝑃 prefix ( 𝐿 + 1 ) ) ↔ ( ( 𝐹 prefix 𝐿 ) ∈ Word dom ( iEdg β€˜ 𝐺 ) ∧ ( 𝑃 prefix ( 𝐿 + 1 ) ) : ( 0 ... ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) ⟢ ( Vtx β€˜ 𝐺 ) ∧ βˆ€ π‘˜ ∈ ( 0 ..^ ( β™― β€˜ ( 𝐹 prefix 𝐿 ) ) ) if- ( ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) = ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) , ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) = { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) } , { ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ π‘˜ ) , ( ( 𝑃 prefix ( 𝐿 + 1 ) ) β€˜ ( π‘˜ + 1 ) ) } βŠ† ( ( iEdg β€˜ 𝐺 ) β€˜ ( ( 𝐹 prefix 𝐿 ) β€˜ π‘˜ ) ) ) ) ) )
104 5 35 98 103 mpbir3and ⊒ ( ( 𝐹 ( Walks β€˜ 𝐺 ) 𝑃 ∧ 𝐿 ∈ ( 0 ... ( β™― β€˜ 𝐹 ) ) ) β†’ ( 𝐹 prefix 𝐿 ) ( Walks β€˜ 𝐺 ) ( 𝑃 prefix ( 𝐿 + 1 ) ) )