Metamath Proof Explorer

Theorem wlk1walk

Description: A walk is a 1-walk "on the edge level" according to Aksoy et al. (Contributed by AV, 30-Dec-2020)

Ref Expression
Hypothesis wlk1walk.i ⊢I=iEdg⁡G
Assertion wlk1walk ⊢FWalks⁡GP→∀k∈1..^F1≤I⁡F⁡k−1∩I⁡F⁡k

Proof

Step Hyp Ref Expression
1 wlk1walk.i ⊢I=iEdg⁡G
2 wlkv ⊢FWalks⁡GP→G∈V∧F∈V∧P∈V
3 eqid ⊢Vtx⁡G=Vtx⁡G
4 eqid ⊢iEdg⁡G=iEdg⁡G
5 3 4 iswlk ⊢G∈V∧F∈V∧P∈V→FWalks⁡GP↔F∈Worddom⁡iEdg⁡G∧P:0…F⟶Vtx⁡G∧∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i
6 fvex ⊢I⁡F⁡k−1∈V
7 6 inex1 ⊢I⁡F⁡k−1∩I⁡F⁡k∈V
8 fzo0ss1 ⊢1..^F⊆0..^F
9 8 sseli ⊢k∈1..^F→k∈0..^F
10 wkslem1 ⊢i=k→if-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i↔if-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k
11 10 rspcv ⊢k∈0..^F→∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i→if-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k
12 9 11 syl ⊢k∈1..^F→∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i→if-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k
13 12 imp ⊢k∈1..^F∧∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i→if-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k
14 elfzofz ⊢k∈1..^F→k∈1…F
15 fz1fzo0m1 ⊢k∈1…F→k−1∈0..^F
16 wkslem1 ⊢i=k−1→if-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i↔if-P⁡k−1=P⁡k-1+1iEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k-1+1⊆iEdg⁡G⁡F⁡k−1
17 16 rspcv ⊢k−1∈0..^F→∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i→if-P⁡k−1=P⁡k-1+1iEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k-1+1⊆iEdg⁡G⁡F⁡k−1
18 14 15 17 3syl ⊢k∈1..^F→∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i→if-P⁡k−1=P⁡k-1+1iEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k-1+1⊆iEdg⁡G⁡F⁡k−1
19 18 imp ⊢k∈1..^F∧∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i→if-P⁡k−1=P⁡k-1+1iEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k-1+1⊆iEdg⁡G⁡F⁡k−1
20 df-ifp ⊢if-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k↔P⁡k=P⁡k+1∧iEdg⁡G⁡F⁡k=P⁡k∨¬P⁡k=P⁡k+1∧P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k
21 elfzoelz ⊢k∈1..^F→k∈ℤ
22 zcn ⊢k∈ℤ→k∈ℂ
23 eqidd ⊢k∈ℂ→k−1=k−1
24 npcan1 ⊢k∈ℂ→k-1+1=k
25 wkslem2 ⊢k−1=k−1∧k-1+1=k→if-P⁡k−1=P⁡k-1+1iEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k-1+1⊆iEdg⁡G⁡F⁡k−1↔if-P⁡k−1=P⁡kiEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1
26 23 24 25 syl2anc ⊢k∈ℂ→if-P⁡k−1=P⁡k-1+1iEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k-1+1⊆iEdg⁡G⁡F⁡k−1↔if-P⁡k−1=P⁡kiEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1
27 21 22 26 3syl ⊢k∈1..^F→if-P⁡k−1=P⁡k-1+1iEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k-1+1⊆iEdg⁡G⁡F⁡k−1↔if-P⁡k−1=P⁡kiEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1
28 df-ifp ⊢if-P⁡k−1=P⁡kiEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1↔P⁡k−1=P⁡k∧iEdg⁡G⁡F⁡k−1=P⁡k−1∨¬P⁡k−1=P⁡k∧P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1
29 sneq ⊢P⁡k−1=P⁡k→P⁡k−1=P⁡k
30 29 eqeq2d ⊢P⁡k−1=P⁡k→iEdg⁡G⁡F⁡k−1=P⁡k−1↔iEdg⁡G⁡F⁡k−1=P⁡k
31 fvex ⊢P⁡k∈V
32 31 snid ⊢P⁡k∈P⁡k
33 1 fveq1i ⊢I⁡F⁡k−1=iEdg⁡G⁡F⁡k−1
34 33 eleq2i ⊢P⁡k∈I⁡F⁡k−1↔P⁡k∈iEdg⁡G⁡F⁡k−1
35 eleq2 ⊢iEdg⁡G⁡F⁡k−1=P⁡k→P⁡k∈iEdg⁡G⁡F⁡k−1↔P⁡k∈P⁡k
36 34 35 bitrid ⊢iEdg⁡G⁡F⁡k−1=P⁡k→P⁡k∈I⁡F⁡k−1↔P⁡k∈P⁡k
37 32 36 mpbiri ⊢iEdg⁡G⁡F⁡k−1=P⁡k→P⁡k∈I⁡F⁡k−1
38 eleq2 ⊢iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈iEdg⁡G⁡F⁡k↔P⁡k∈P⁡k
39 32 38 mpbiri ⊢iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈iEdg⁡G⁡F⁡k
40 1 fveq1i ⊢I⁡F⁡k=iEdg⁡G⁡F⁡k
41 39 40 eleqtrrdi ⊢iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈I⁡F⁡k
42 37 41 anim12i ⊢iEdg⁡G⁡F⁡k−1=P⁡k∧iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
43 42 ex ⊢iEdg⁡G⁡F⁡k−1=P⁡k→iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
44 30 43 syl6bi ⊢P⁡k−1=P⁡k→iEdg⁡G⁡F⁡k−1=P⁡k−1→iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
45 44 imp ⊢P⁡k−1=P⁡k∧iEdg⁡G⁡F⁡k−1=P⁡k−1→iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
46 45 com12 ⊢iEdg⁡G⁡F⁡k=P⁡k→P⁡k−1=P⁡k∧iEdg⁡G⁡F⁡k−1=P⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
47 46 adantl ⊢P⁡k=P⁡k+1∧iEdg⁡G⁡F⁡k=P⁡k→P⁡k−1=P⁡k∧iEdg⁡G⁡F⁡k−1=P⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
48 fvex ⊢P⁡k+1∈V
49 31 48 prss ⊢P⁡k∈iEdg⁡G⁡F⁡k∧P⁡k+1∈iEdg⁡G⁡F⁡k↔P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k
50 1 eqcomi ⊢iEdg⁡G=I
51 50 fveq1i ⊢iEdg⁡G⁡F⁡k=I⁡F⁡k
52 51 eleq2i ⊢P⁡k∈iEdg⁡G⁡F⁡k↔P⁡k∈I⁡F⁡k
53 52 biimpi ⊢P⁡k∈iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k
54 53 adantr ⊢P⁡k∈iEdg⁡G⁡F⁡k∧P⁡k+1∈iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k
55 49 54 sylbir ⊢P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k
56 37 55 anim12i ⊢iEdg⁡G⁡F⁡k−1=P⁡k∧P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
57 56 ex ⊢iEdg⁡G⁡F⁡k−1=P⁡k→P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
58 30 57 syl6bi ⊢P⁡k−1=P⁡k→iEdg⁡G⁡F⁡k−1=P⁡k−1→P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
59 58 imp ⊢P⁡k−1=P⁡k∧iEdg⁡G⁡F⁡k−1=P⁡k−1→P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
60 59 com12 ⊢P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡k−1=P⁡k∧iEdg⁡G⁡F⁡k−1=P⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
61 60 adantl ⊢¬P⁡k=P⁡k+1∧P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡k−1=P⁡k∧iEdg⁡G⁡F⁡k−1=P⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
62 47 61 jaoi ⊢P⁡k=P⁡k+1∧iEdg⁡G⁡F⁡k=P⁡k∨¬P⁡k=P⁡k+1∧P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡k−1=P⁡k∧iEdg⁡G⁡F⁡k−1=P⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
63 62 com12 ⊢P⁡k−1=P⁡k∧iEdg⁡G⁡F⁡k−1=P⁡k−1→P⁡k=P⁡k+1∧iEdg⁡G⁡F⁡k=P⁡k∨¬P⁡k=P⁡k+1∧P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
64 fvex ⊢P⁡k−1∈V
65 64 31 prss ⊢P⁡k−1∈iEdg⁡G⁡F⁡k−1∧P⁡k∈iEdg⁡G⁡F⁡k−1↔P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1
66 50 fveq1i ⊢iEdg⁡G⁡F⁡k−1=I⁡F⁡k−1
67 66 eleq2i ⊢P⁡k∈iEdg⁡G⁡F⁡k−1↔P⁡k∈I⁡F⁡k−1
68 67 biimpi ⊢P⁡k∈iEdg⁡G⁡F⁡k−1→P⁡k∈I⁡F⁡k−1
69 40 eleq2i ⊢P⁡k∈I⁡F⁡k↔P⁡k∈iEdg⁡G⁡F⁡k
70 69 38 bitrid ⊢iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈I⁡F⁡k↔P⁡k∈P⁡k
71 32 70 mpbiri ⊢iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈I⁡F⁡k
72 68 71 anim12i ⊢P⁡k∈iEdg⁡G⁡F⁡k−1∧iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
73 72 ex ⊢P⁡k∈iEdg⁡G⁡F⁡k−1→iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
74 73 adantl ⊢P⁡k−1∈iEdg⁡G⁡F⁡k−1∧P⁡k∈iEdg⁡G⁡F⁡k−1→iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
75 65 74 sylbir ⊢P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
76 75 adantl ⊢¬P⁡k−1=P⁡k∧P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→iEdg⁡G⁡F⁡k=P⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
77 76 com12 ⊢iEdg⁡G⁡F⁡k=P⁡k→¬P⁡k−1=P⁡k∧P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
78 77 adantl ⊢P⁡k=P⁡k+1∧iEdg⁡G⁡F⁡k=P⁡k→¬P⁡k−1=P⁡k∧P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
79 67 52 anbi12i ⊢P⁡k∈iEdg⁡G⁡F⁡k−1∧P⁡k∈iEdg⁡G⁡F⁡k↔P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
80 79 biimpi ⊢P⁡k∈iEdg⁡G⁡F⁡k−1∧P⁡k∈iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
81 80 ex ⊢P⁡k∈iEdg⁡G⁡F⁡k−1→P⁡k∈iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
82 81 adantl ⊢P⁡k−1∈iEdg⁡G⁡F⁡k−1∧P⁡k∈iEdg⁡G⁡F⁡k−1→P⁡k∈iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
83 65 82 sylbir ⊢P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→P⁡k∈iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
84 83 adantl ⊢¬P⁡k−1=P⁡k∧P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→P⁡k∈iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
85 84 com12 ⊢P⁡k∈iEdg⁡G⁡F⁡k→¬P⁡k−1=P⁡k∧P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
86 85 adantr ⊢P⁡k∈iEdg⁡G⁡F⁡k∧P⁡k+1∈iEdg⁡G⁡F⁡k→¬P⁡k−1=P⁡k∧P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
87 49 86 sylbir ⊢P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→¬P⁡k−1=P⁡k∧P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
88 87 adantl ⊢¬P⁡k=P⁡k+1∧P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→¬P⁡k−1=P⁡k∧P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
89 78 88 jaoi ⊢P⁡k=P⁡k+1∧iEdg⁡G⁡F⁡k=P⁡k∨¬P⁡k=P⁡k+1∧P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→¬P⁡k−1=P⁡k∧P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
90 89 com12 ⊢¬P⁡k−1=P⁡k∧P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→P⁡k=P⁡k+1∧iEdg⁡G⁡F⁡k=P⁡k∨¬P⁡k=P⁡k+1∧P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
91 63 90 jaoi ⊢P⁡k−1=P⁡k∧iEdg⁡G⁡F⁡k−1=P⁡k−1∨¬P⁡k−1=P⁡k∧P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→P⁡k=P⁡k+1∧iEdg⁡G⁡F⁡k=P⁡k∨¬P⁡k=P⁡k+1∧P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
92 28 91 sylbi ⊢if-P⁡k−1=P⁡kiEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k⊆iEdg⁡G⁡F⁡k−1→P⁡k=P⁡k+1∧iEdg⁡G⁡F⁡k=P⁡k∨¬P⁡k=P⁡k+1∧P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
93 27 92 syl6bi ⊢k∈1..^F→if-P⁡k−1=P⁡k-1+1iEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k-1+1⊆iEdg⁡G⁡F⁡k−1→P⁡k=P⁡k+1∧iEdg⁡G⁡F⁡k=P⁡k∨¬P⁡k=P⁡k+1∧P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
94 93 com3r ⊢P⁡k=P⁡k+1∧iEdg⁡G⁡F⁡k=P⁡k∨¬P⁡k=P⁡k+1∧P⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→k∈1..^F→if-P⁡k−1=P⁡k-1+1iEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k-1+1⊆iEdg⁡G⁡F⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
95 20 94 sylbi ⊢if-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→k∈1..^F→if-P⁡k−1=P⁡k-1+1iEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k-1+1⊆iEdg⁡G⁡F⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
96 95 com12 ⊢k∈1..^F→if-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→if-P⁡k−1=P⁡k-1+1iEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k-1+1⊆iEdg⁡G⁡F⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
97 96 adantr ⊢k∈1..^F∧∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i→if-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→if-P⁡k−1=P⁡k-1+1iEdg⁡G⁡F⁡k−1=P⁡k−1P⁡k−1P⁡k-1+1⊆iEdg⁡G⁡F⁡k−1→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
98 13 19 97 mp2d ⊢k∈1..^F∧∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
99 98 ancoms ⊢∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i∧k∈1..^F→P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k
100 inelcm ⊢P⁡k∈I⁡F⁡k−1∧P⁡k∈I⁡F⁡k→I⁡F⁡k−1∩I⁡F⁡k≠∅
101 99 100 syl ⊢∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i∧k∈1..^F→I⁡F⁡k−1∩I⁡F⁡k≠∅
102 hashge1 ⊢I⁡F⁡k−1∩I⁡F⁡k∈V∧I⁡F⁡k−1∩I⁡F⁡k≠∅→1≤I⁡F⁡k−1∩I⁡F⁡k
103 7 101 102 sylancr ⊢∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i∧k∈1..^F→1≤I⁡F⁡k−1∩I⁡F⁡k
104 103 ralrimiva ⊢∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i→∀k∈1..^F1≤I⁡F⁡k−1∩I⁡F⁡k
105 104 3ad2ant3 ⊢F∈Worddom⁡iEdg⁡G∧P:0…F⟶Vtx⁡G∧∀i∈0..^Fif-P⁡i=P⁡i+1iEdg⁡G⁡F⁡i=P⁡iP⁡iP⁡i+1⊆iEdg⁡G⁡F⁡i→∀k∈1..^F1≤I⁡F⁡k−1∩I⁡F⁡k
106 5 105 syl6bi ⊢G∈V∧F∈V∧P∈V→FWalks⁡GP→∀k∈1..^F1≤I⁡F⁡k−1∩I⁡F⁡k
107 2 106 mpcom ⊢FWalks⁡GP→∀k∈1..^F1≤I⁡F⁡k−1∩I⁡F⁡k