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 ⊢ F Walks ⁡ G P → ∀ k ∈ 1 ..^ F 1 ≤ I ⁡ F ⁡ k − 1 ∩ I ⁡ F ⁡ k

Proof

Step Hyp Ref Expression
1 wlk1walk.i ⊢ I = iEdg ⁡ G
2 wlkv ⊢ F Walks ⁡ G P → 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 → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ 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 + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ i ↔ if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k
11 10 rspcv ⊢ k ∈ 0 ..^ F → ∀ i ∈ 0 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ i → if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k
12 9 11 syl ⊢ k ∈ 1 ..^ F → ∀ i ∈ 0 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ i → if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k
13 12 imp ⊢ k ∈ 1 ..^ F ∧ ∀ i ∈ 0 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ i → if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ 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 + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ i ↔ if- P ⁡ k − 1 = P ⁡ k - 1 + 1 iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ k - 1 + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1
17 16 rspcv ⊢ k − 1 ∈ 0 ..^ F → ∀ i ∈ 0 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ i → if- P ⁡ k − 1 = P ⁡ k - 1 + 1 iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ k - 1 + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1
18 14 15 17 3syl ⊢ k ∈ 1 ..^ F → ∀ i ∈ 0 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ i → if- P ⁡ k − 1 = P ⁡ k - 1 + 1 iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ k - 1 + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1
19 18 imp ⊢ k ∈ 1 ..^ F ∧ ∀ i ∈ 0 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ i → if- P ⁡ k − 1 = P ⁡ k - 1 + 1 iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ k - 1 + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1
20 df-ifp ⊢ if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k ↔ P ⁡ k = P ⁡ k + 1 ∧ iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k ∨ ¬ P ⁡ k = P ⁡ k + 1 ∧ P ⁡ k P ⁡ 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 + 1 iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ k - 1 + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1 ↔ if- P ⁡ k − 1 = P ⁡ k iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ k ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1
26 23 24 25 syl2anc ⊢ k ∈ ℂ → if- P ⁡ k − 1 = P ⁡ k - 1 + 1 iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ k - 1 + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1 ↔ if- P ⁡ k − 1 = P ⁡ k iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ k ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1
27 21 22 26 3syl ⊢ k ∈ 1 ..^ F → if- P ⁡ k − 1 = P ⁡ k - 1 + 1 iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ k - 1 + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1 ↔ if- P ⁡ k − 1 = P ⁡ k iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ k ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1
28 df-ifp ⊢ if- P ⁡ k − 1 = P ⁡ k iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ 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 − 1 P ⁡ 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 syl5bb ⊢ 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 ⁡ k P ⁡ 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 ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k → P ⁡ k ∈ I ⁡ F ⁡ k
56 37 55 anim12i ⊢ iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k ∧ P ⁡ k P ⁡ 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 ⁡ k P ⁡ 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 ⁡ k P ⁡ 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 ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k → P ⁡ k ∈ I ⁡ F ⁡ k − 1 ∧ P ⁡ k ∈ I ⁡ F ⁡ k
60 59 com12 ⊢ P ⁡ k P ⁡ 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 ⁡ k P ⁡ 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 ⁡ k P ⁡ 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 ⁡ k P ⁡ 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 − 1 P ⁡ 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 syl5bb ⊢ 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 − 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
76 75 adantl ⊢ ¬ P ⁡ k − 1 = P ⁡ k ∧ P ⁡ 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
77 76 com12 ⊢ iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k → ¬ P ⁡ k − 1 = P ⁡ k ∧ P ⁡ k − 1 P ⁡ 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 − 1 P ⁡ 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 − 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
84 83 adantl ⊢ ¬ P ⁡ k − 1 = P ⁡ k ∧ P ⁡ 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
85 84 com12 ⊢ P ⁡ k ∈ iEdg ⁡ G ⁡ F ⁡ k → ¬ P ⁡ k − 1 = P ⁡ k ∧ P ⁡ k − 1 P ⁡ 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 − 1 P ⁡ k ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1 → P ⁡ k ∈ I ⁡ F ⁡ k − 1 ∧ P ⁡ k ∈ I ⁡ F ⁡ k
87 49 86 sylbir ⊢ P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k → ¬ P ⁡ k − 1 = P ⁡ k ∧ P ⁡ k − 1 P ⁡ 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 ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k → ¬ P ⁡ k − 1 = P ⁡ k ∧ P ⁡ k − 1 P ⁡ 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 ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k → ¬ P ⁡ k − 1 = P ⁡ k ∧ P ⁡ k − 1 P ⁡ 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 − 1 P ⁡ k ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1 → P ⁡ k = P ⁡ k + 1 ∧ iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k ∨ ¬ P ⁡ k = P ⁡ k + 1 ∧ P ⁡ k P ⁡ 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 − 1 P ⁡ k ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1 → P ⁡ k = P ⁡ k + 1 ∧ iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k ∨ ¬ P ⁡ k = P ⁡ k + 1 ∧ P ⁡ k P ⁡ 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 ⁡ k iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ k ⊆ iEdg ⁡ G ⁡ F ⁡ k − 1 → P ⁡ k = P ⁡ k + 1 ∧ iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k ∨ ¬ P ⁡ k = P ⁡ k + 1 ∧ P ⁡ k P ⁡ 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 + 1 iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ 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 ⁡ k P ⁡ 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 ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k → k ∈ 1 ..^ F → if- P ⁡ k − 1 = P ⁡ k - 1 + 1 iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ 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 + 1 iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k → k ∈ 1 ..^ F → if- P ⁡ k − 1 = P ⁡ k - 1 + 1 iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ 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 + 1 iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k → if- P ⁡ k − 1 = P ⁡ k - 1 + 1 iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ 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 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ i → if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k → if- P ⁡ k − 1 = P ⁡ k - 1 + 1 iEdg ⁡ G ⁡ F ⁡ k − 1 = P ⁡ k − 1 P ⁡ k − 1 P ⁡ 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 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ i → P ⁡ k ∈ I ⁡ F ⁡ k − 1 ∧ P ⁡ k ∈ I ⁡ F ⁡ k
99 98 ancoms ⊢ ∀ i ∈ 0 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ 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 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ 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 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ i ∧ k ∈ 1 ..^ F → 1 ≤ I ⁡ F ⁡ k − 1 ∩ I ⁡ F ⁡ k
104 103 ralrimiva ⊢ ∀ i ∈ 0 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ i → ∀ k ∈ 1 ..^ F 1 ≤ I ⁡ F ⁡ k − 1 ∩ I ⁡ F ⁡ k
105 104 3ad2ant3 ⊢ F ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ F if- P ⁡ i = P ⁡ i + 1 iEdg ⁡ G ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ i → ∀ k ∈ 1 ..^ F 1 ≤ I ⁡ F ⁡ k − 1 ∩ I ⁡ F ⁡ k
106 5 105 syl6bi ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F Walks ⁡ G P → ∀ k ∈ 1 ..^ F 1 ≤ I ⁡ F ⁡ k − 1 ∩ I ⁡ F ⁡ k
107 2 106 mpcom ⊢ F Walks ⁡ G P → ∀ k ∈ 1 ..^ F 1 ≤ I ⁡ F ⁡ k − 1 ∩ I ⁡ F ⁡ k