# 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}=\mathrm{iEdg}\left({G}\right)$
Assertion wlk1walk ${⊢}{F}\mathrm{Walks}\left({G}\right){P}\to \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}1\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|$

### Proof

Step Hyp Ref Expression
1 wlk1walk.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
2 wlkv ${⊢}{F}\mathrm{Walks}\left({G}\right){P}\to \left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)$
3 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
4 eqid ${⊢}\mathrm{iEdg}\left({G}\right)=\mathrm{iEdg}\left({G}\right)$
5 3 4 iswlk ${⊢}\left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)\to \left({F}\mathrm{Walks}\left({G}\right){P}↔\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge {P}:\left(0\dots \left|{F}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\right)\right)$
6 fvex ${⊢}{I}\left({F}\left({k}-1\right)\right)\in \mathrm{V}$
7 6 inex1 ${⊢}{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\in \mathrm{V}$
8 fzo0ss1 ${⊢}\left(1..^\left|{F}\right|\right)\subseteq \left(0..^\left|{F}\right|\right)$
9 8 sseli ${⊢}{k}\in \left(1..^\left|{F}\right|\right)\to {k}\in \left(0..^\left|{F}\right|\right)$
10 wkslem1 ${⊢}{i}={k}\to \left(if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)↔if-\left({P}\left({k}\right)={P}\left({k}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\},\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\right)$
11 10 rspcv ${⊢}{k}\in \left(0..^\left|{F}\right|\right)\to \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\to if-\left({P}\left({k}\right)={P}\left({k}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\},\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\right)$
12 9 11 syl ${⊢}{k}\in \left(1..^\left|{F}\right|\right)\to \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\to if-\left({P}\left({k}\right)={P}\left({k}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\},\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\right)$
13 12 imp ${⊢}\left({k}\in \left(1..^\left|{F}\right|\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\right)\to if-\left({P}\left({k}\right)={P}\left({k}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\},\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)$
14 elfzofz ${⊢}{k}\in \left(1..^\left|{F}\right|\right)\to {k}\in \left(1\dots \left|{F}\right|\right)$
15 fz1fzo0m1 ${⊢}{k}\in \left(1\dots \left|{F}\right|\right)\to {k}-1\in \left(0..^\left|{F}\right|\right)$
16 wkslem1 ${⊢}{i}={k}-1\to \left(if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)↔if-\left({P}\left({k}-1\right)={P}\left({k}-1+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}-1+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\right)$
17 16 rspcv ${⊢}{k}-1\in \left(0..^\left|{F}\right|\right)\to \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\to if-\left({P}\left({k}-1\right)={P}\left({k}-1+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}-1+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\right)$
18 14 15 17 3syl ${⊢}{k}\in \left(1..^\left|{F}\right|\right)\to \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\to if-\left({P}\left({k}-1\right)={P}\left({k}-1+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}-1+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\right)$
19 18 imp ${⊢}\left({k}\in \left(1..^\left|{F}\right|\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\right)\to if-\left({P}\left({k}-1\right)={P}\left({k}-1+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}-1+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)$
20 df-ifp ${⊢}if-\left({P}\left({k}\right)={P}\left({k}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\},\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)↔\left(\left({P}\left({k}\right)={P}\left({k}+1\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\right)\vee \left(¬{P}\left({k}\right)={P}\left({k}+1\right)\wedge \left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\right)$
21 elfzoelz ${⊢}{k}\in \left(1..^\left|{F}\right|\right)\to {k}\in ℤ$
22 zcn ${⊢}{k}\in ℤ\to {k}\in ℂ$
23 eqidd ${⊢}{k}\in ℂ\to {k}-1={k}-1$
24 npcan1 ${⊢}{k}\in ℂ\to {k}-1+1={k}$
25 wkslem2 ${⊢}\left({k}-1={k}-1\wedge {k}-1+1={k}\right)\to \left(if-\left({P}\left({k}-1\right)={P}\left({k}-1+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}-1+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)↔if-\left({P}\left({k}-1\right)={P}\left({k}\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\right)$
26 23 24 25 syl2anc ${⊢}{k}\in ℂ\to \left(if-\left({P}\left({k}-1\right)={P}\left({k}-1+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}-1+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)↔if-\left({P}\left({k}-1\right)={P}\left({k}\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\right)$
27 21 22 26 3syl ${⊢}{k}\in \left(1..^\left|{F}\right|\right)\to \left(if-\left({P}\left({k}-1\right)={P}\left({k}-1+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}-1+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)↔if-\left({P}\left({k}-1\right)={P}\left({k}\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\right)$
28 df-ifp ${⊢}if-\left({P}\left({k}-1\right)={P}\left({k}\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)↔\left(\left({P}\left({k}-1\right)={P}\left({k}\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\}\right)\vee \left(¬{P}\left({k}-1\right)={P}\left({k}\right)\wedge \left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\right)$
29 sneq ${⊢}{P}\left({k}-1\right)={P}\left({k}\right)\to \left\{{P}\left({k}-1\right)\right\}=\left\{{P}\left({k}\right)\right\}$
30 29 eqeq2d ${⊢}{P}\left({k}-1\right)={P}\left({k}\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\}↔\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}\right)\right\}\right)$
31 fvex ${⊢}{P}\left({k}\right)\in \mathrm{V}$
32 31 snid ${⊢}{P}\left({k}\right)\in \left\{{P}\left({k}\right)\right\}$
33 1 fveq1i ${⊢}{I}\left({F}\left({k}-1\right)\right)=\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)$
34 33 eleq2i ${⊢}{P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)↔{P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)$
35 eleq2 ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left({P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)↔{P}\left({k}\right)\in \left\{{P}\left({k}\right)\right\}\right)$
36 34 35 syl5bb ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)↔{P}\left({k}\right)\in \left\{{P}\left({k}\right)\right\}\right)$
37 32 36 mpbiri ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}\right)\right\}\to {P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)$
38 eleq2 ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left({P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)↔{P}\left({k}\right)\in \left\{{P}\left({k}\right)\right\}\right)$
39 32 38 mpbiri ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to {P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)$
40 1 fveq1i ${⊢}{I}\left({F}\left({k}\right)\right)=\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)$
41 39 40 eleqtrrdi ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)$
42 37 41 anim12i ${⊢}\left(\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)$
43 42 ex ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
44 30 43 syl6bi ${⊢}{P}\left({k}-1\right)={P}\left({k}\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\}\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)\right)$
45 44 imp ${⊢}\left({P}\left({k}-1\right)={P}\left({k}\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\}\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
46 45 com12 ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left(\left({P}\left({k}-1\right)={P}\left({k}\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\}\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
47 46 adantl ${⊢}\left({P}\left({k}\right)={P}\left({k}+1\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\right)\to \left(\left({P}\left({k}-1\right)={P}\left({k}\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\}\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
48 fvex ${⊢}{P}\left({k}+1\right)\in \mathrm{V}$
49 31 48 prss ${⊢}\left({P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\wedge {P}\left({k}+1\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)↔\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)$
50 1 eqcomi ${⊢}\mathrm{iEdg}\left({G}\right)={I}$
51 50 fveq1i ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)={I}\left({F}\left({k}\right)\right)$
52 51 eleq2i ${⊢}{P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)↔{P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)$
53 52 biimpi ${⊢}{P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\to {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)$
54 53 adantr ${⊢}\left({P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\wedge {P}\left({k}+1\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\to {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)$
55 49 54 sylbir ${⊢}\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\to {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)$
56 37 55 anim12i ${⊢}\left(\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}\right)\right\}\wedge \left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)$
57 56 ex ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left(\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
58 30 57 syl6bi ${⊢}{P}\left({k}-1\right)={P}\left({k}\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\}\to \left(\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)\right)$
59 58 imp ${⊢}\left({P}\left({k}-1\right)={P}\left({k}\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\}\right)\to \left(\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
60 59 com12 ${⊢}\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\to \left(\left({P}\left({k}-1\right)={P}\left({k}\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\}\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
61 60 adantl ${⊢}\left(¬{P}\left({k}\right)={P}\left({k}+1\right)\wedge \left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\to \left(\left({P}\left({k}-1\right)={P}\left({k}\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\}\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
62 47 61 jaoi ${⊢}\left(\left({P}\left({k}\right)={P}\left({k}+1\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\right)\vee \left(¬{P}\left({k}\right)={P}\left({k}+1\right)\wedge \left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\right)\to \left(\left({P}\left({k}-1\right)={P}\left({k}\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\}\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
63 62 com12 ${⊢}\left({P}\left({k}-1\right)={P}\left({k}\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\}\right)\to \left(\left(\left({P}\left({k}\right)={P}\left({k}+1\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\right)\vee \left(¬{P}\left({k}\right)={P}\left({k}+1\right)\wedge \left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
64 fvex ${⊢}{P}\left({k}-1\right)\in \mathrm{V}$
65 64 31 prss ${⊢}\left({P}\left({k}-1\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)↔\left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)$
66 50 fveq1i ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)={I}\left({F}\left({k}-1\right)\right)$
67 66 eleq2i ${⊢}{P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)↔{P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)$
68 67 biimpi ${⊢}{P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\to {P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)$
69 40 eleq2i ${⊢}{P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)↔{P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)$
70 69 38 syl5bb ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)↔{P}\left({k}\right)\in \left\{{P}\left({k}\right)\right\}\right)$
71 32 70 mpbiri ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)$
72 68 71 anim12i ${⊢}\left({P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)$
73 72 ex ${⊢}{P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
74 73 adantl ${⊢}\left({P}\left({k}-1\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
75 65 74 sylbir ${⊢}\left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
76 75 adantl ${⊢}\left(¬{P}\left({k}-1\right)={P}\left({k}\right)\wedge \left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
77 76 com12 ${⊢}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\to \left(\left(¬{P}\left({k}-1\right)={P}\left({k}\right)\wedge \left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
78 77 adantl ${⊢}\left({P}\left({k}\right)={P}\left({k}+1\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\right)\to \left(\left(¬{P}\left({k}-1\right)={P}\left({k}\right)\wedge \left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
79 67 52 anbi12i ${⊢}\left({P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)↔\left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)$
80 79 biimpi ${⊢}\left({P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)$
81 80 ex ${⊢}{P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\to \left({P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
82 81 adantl ${⊢}\left({P}\left({k}-1\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left({P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
83 65 82 sylbir ${⊢}\left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\to \left({P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
84 83 adantl ${⊢}\left(¬{P}\left({k}-1\right)={P}\left({k}\right)\wedge \left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left({P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
85 84 com12 ${⊢}{P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\to \left(\left(¬{P}\left({k}-1\right)={P}\left({k}\right)\wedge \left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
86 85 adantr ${⊢}\left({P}\left({k}\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\wedge {P}\left({k}+1\right)\in \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\to \left(\left(¬{P}\left({k}-1\right)={P}\left({k}\right)\wedge \left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
87 49 86 sylbir ${⊢}\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\to \left(\left(¬{P}\left({k}-1\right)={P}\left({k}\right)\wedge \left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
88 87 adantl ${⊢}\left(¬{P}\left({k}\right)={P}\left({k}+1\right)\wedge \left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\to \left(\left(¬{P}\left({k}-1\right)={P}\left({k}\right)\wedge \left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
89 78 88 jaoi ${⊢}\left(\left({P}\left({k}\right)={P}\left({k}+1\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\right)\vee \left(¬{P}\left({k}\right)={P}\left({k}+1\right)\wedge \left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\right)\to \left(\left(¬{P}\left({k}-1\right)={P}\left({k}\right)\wedge \left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
90 89 com12 ${⊢}\left(¬{P}\left({k}-1\right)={P}\left({k}\right)\wedge \left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left(\left(\left({P}\left({k}\right)={P}\left({k}+1\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\right)\vee \left(¬{P}\left({k}\right)={P}\left({k}+1\right)\wedge \left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
91 63 90 jaoi ${⊢}\left(\left({P}\left({k}-1\right)={P}\left({k}\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\}\right)\vee \left(¬{P}\left({k}-1\right)={P}\left({k}\right)\wedge \left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\right)\to \left(\left(\left({P}\left({k}\right)={P}\left({k}+1\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\right)\vee \left(¬{P}\left({k}\right)={P}\left({k}+1\right)\wedge \left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
92 28 91 sylbi ${⊢}if-\left({P}\left({k}-1\right)={P}\left({k}\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left(\left(\left({P}\left({k}\right)={P}\left({k}+1\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\right)\vee \left(¬{P}\left({k}\right)={P}\left({k}+1\right)\wedge \left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)$
93 27 92 syl6bi ${⊢}{k}\in \left(1..^\left|{F}\right|\right)\to \left(if-\left({P}\left({k}-1\right)={P}\left({k}-1+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}-1+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left(\left(\left({P}\left({k}\right)={P}\left({k}+1\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\right)\vee \left(¬{P}\left({k}\right)={P}\left({k}+1\right)\wedge \left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)\right)$
94 93 com3r ${⊢}\left(\left({P}\left({k}\right)={P}\left({k}+1\right)\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\}\right)\vee \left(¬{P}\left({k}\right)={P}\left({k}+1\right)\wedge \left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\right)\to \left({k}\in \left(1..^\left|{F}\right|\right)\to \left(if-\left({P}\left({k}-1\right)={P}\left({k}-1+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}-1+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)\right)$
95 20 94 sylbi ${⊢}if-\left({P}\left({k}\right)={P}\left({k}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\},\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\to \left({k}\in \left(1..^\left|{F}\right|\right)\to \left(if-\left({P}\left({k}-1\right)={P}\left({k}-1+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}-1+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)\right)$
96 95 com12 ${⊢}{k}\in \left(1..^\left|{F}\right|\right)\to \left(if-\left({P}\left({k}\right)={P}\left({k}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\},\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\to \left(if-\left({P}\left({k}-1\right)={P}\left({k}-1+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}-1+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)\right)$
97 96 adantr ${⊢}\left({k}\in \left(1..^\left|{F}\right|\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\right)\to \left(if-\left({P}\left({k}\right)={P}\left({k}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right)\right\},\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)\right)\to \left(if-\left({P}\left({k}-1\right)={P}\left({k}-1+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)=\left\{{P}\left({k}-1\right)\right\},\left\{{P}\left({k}-1\right),{P}\left({k}-1+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({k}-1\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\right)\right)$
98 13 19 97 mp2d ${⊢}\left({k}\in \left(1..^\left|{F}\right|\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)$
99 98 ancoms ${⊢}\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\wedge {k}\in \left(1..^\left|{F}\right|\right)\right)\to \left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)$
100 inelcm ${⊢}\left({P}\left({k}\right)\in {I}\left({F}\left({k}-1\right)\right)\wedge {P}\left({k}\right)\in {I}\left({F}\left({k}\right)\right)\right)\to {I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\ne \varnothing$
101 99 100 syl ${⊢}\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\wedge {k}\in \left(1..^\left|{F}\right|\right)\right)\to {I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\ne \varnothing$
102 hashge1 ${⊢}\left({I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\in \mathrm{V}\wedge {I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\ne \varnothing \right)\to 1\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|$
103 7 101 102 sylancr ${⊢}\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\wedge {k}\in \left(1..^\left|{F}\right|\right)\right)\to 1\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|$
104 103 ralrimiva ${⊢}\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\to \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}1\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|$
105 104 3ad2ant3 ${⊢}\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge {P}:\left(0\dots \left|{F}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),\mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq \mathrm{iEdg}\left({G}\right)\left({F}\left({i}\right)\right)\right)\right)\to \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}1\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|$
106 5 105 syl6bi ${⊢}\left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)\to \left({F}\mathrm{Walks}\left({G}\right){P}\to \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}1\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|\right)$
107 2 106 mpcom ${⊢}{F}\mathrm{Walks}\left({G}\right){P}\to \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}1\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|$