# Metamath Proof Explorer

## Theorem clwlkclwwlklem2

Description: Lemma 2 for clwlkclwwlk . (Contributed by Alexander van der Vekens, 22-Jun-2018) (Revised by AV, 11-Apr-2021)

Ref Expression
Assertion clwlkclwwlklem2 ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left({P}:\left(0\dots \left|{F}\right|\right)⟶{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)$

### Proof

Step Hyp Ref Expression
1 f1fn ${⊢}{E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\to {E}Fn\mathrm{dom}{E}$
2 dffn3 ${⊢}{E}Fn\mathrm{dom}{E}↔{E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}$
3 1 2 sylib ${⊢}{E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\to {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}$
4 lencl ${⊢}{F}\in \mathrm{Word}\mathrm{dom}{E}\to \left|{F}\right|\in {ℕ}_{0}$
5 ffn ${⊢}{P}:\left(0\dots \left|{F}\right|\right)⟶{V}\to {P}Fn\left(0\dots \left|{F}\right|\right)$
6 fnfz0hash ${⊢}\left(\left|{F}\right|\in {ℕ}_{0}\wedge {P}Fn\left(0\dots \left|{F}\right|\right)\right)\to \left|{P}\right|=\left|{F}\right|+1$
7 4 5 6 syl2an ${⊢}\left({F}\in \mathrm{Word}\mathrm{dom}{E}\wedge {P}:\left(0\dots \left|{F}\right|\right)⟶{V}\right)\to \left|{P}\right|=\left|{F}\right|+1$
8 ffz0iswrd ${⊢}{P}:\left(0\dots \left|{F}\right|\right)⟶{V}\to {P}\in \mathrm{Word}{V}$
9 lsw ${⊢}{P}\in \mathrm{Word}{V}\to \mathrm{lastS}\left({P}\right)={P}\left(\left|{P}\right|-1\right)$
10 9 ad6antr ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\right)\to \mathrm{lastS}\left({P}\right)={P}\left(\left|{P}\right|-1\right)$
11 fvoveq1 ${⊢}\left|{P}\right|=\left|{F}\right|+1\to {P}\left(\left|{P}\right|-1\right)={P}\left(\left|{F}\right|+1-1\right)$
12 11 ad4antlr ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\right)\to {P}\left(\left|{P}\right|-1\right)={P}\left(\left|{F}\right|+1-1\right)$
13 eqcom ${⊢}{P}\left(0\right)={P}\left(\left|{F}\right|\right)↔{P}\left(\left|{F}\right|\right)={P}\left(0\right)$
14 nn0cn ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left|{F}\right|\in ℂ$
15 1cnd ${⊢}\left|{F}\right|\in {ℕ}_{0}\to 1\in ℂ$
16 14 15 pncand ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left|{F}\right|+1-1=\left|{F}\right|$
17 16 eqcomd ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left|{F}\right|=\left|{F}\right|+1-1$
18 17 ad4antlr ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left|{F}\right|=\left|{F}\right|+1-1$
19 18 fveqeq2d ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left({P}\left(\left|{F}\right|\right)={P}\left(0\right)↔{P}\left(\left|{F}\right|+1-1\right)={P}\left(0\right)\right)$
20 19 biimpd ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left({P}\left(\left|{F}\right|\right)={P}\left(0\right)\to {P}\left(\left|{F}\right|+1-1\right)={P}\left(0\right)\right)$
21 13 20 syl5bi ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left({P}\left(0\right)={P}\left(\left|{F}\right|\right)\to {P}\left(\left|{F}\right|+1-1\right)={P}\left(0\right)\right)$
22 21 adantld ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left(\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to {P}\left(\left|{F}\right|+1-1\right)={P}\left(0\right)\right)$
23 22 imp ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\right)\to {P}\left(\left|{F}\right|+1-1\right)={P}\left(0\right)$
24 10 12 23 3eqtrd ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\right)\to \mathrm{lastS}\left({P}\right)={P}\left(0\right)$
25 nn0z ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left|{F}\right|\in ℤ$
26 peano2zm ${⊢}\left|{F}\right|\in ℤ\to \left|{F}\right|-1\in ℤ$
27 25 26 syl ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left|{F}\right|-1\in ℤ$
28 nn0re ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left|{F}\right|\in ℝ$
29 28 lem1d ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left|{F}\right|-1\le \left|{F}\right|$
30 eluz2 ${⊢}\left|{F}\right|\in {ℤ}_{\ge \left(\left|{F}\right|-1\right)}↔\left(\left|{F}\right|-1\in ℤ\wedge \left|{F}\right|\in ℤ\wedge \left|{F}\right|-1\le \left|{F}\right|\right)$
31 27 25 29 30 syl3anbrc ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left|{F}\right|\in {ℤ}_{\ge \left(\left|{F}\right|-1\right)}$
32 31 ad4antlr ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left|{F}\right|\in {ℤ}_{\ge \left(\left|{F}\right|-1\right)}$
33 fzoss2 ${⊢}\left|{F}\right|\in {ℤ}_{\ge \left(\left|{F}\right|-1\right)}\to \left(0..^\left|{F}\right|-1\right)\subseteq \left(0..^\left|{F}\right|\right)$
34 ssralv ${⊢}\left(0..^\left|{F}\right|-1\right)\subseteq \left(0..^\left|{F}\right|\right)\to \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\to \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)$
35 32 33 34 3syl ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\to \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\right)$
36 simpr ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}$
37 36 adantr ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge {i}\in \left(0..^\left|{F}\right|-1\right)\right)\to {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}$
38 wrdf ${⊢}{F}\in \mathrm{Word}\mathrm{dom}{E}\to {F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{E}$
39 simpll ${⊢}\left(\left({F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{E}\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge {i}\in \left(0..^\left|{F}\right|-1\right)\right)\to {F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{E}$
40 fzossrbm1 ${⊢}\left|{F}\right|\in ℤ\to \left(0..^\left|{F}\right|-1\right)\subseteq \left(0..^\left|{F}\right|\right)$
41 25 40 syl ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left(0..^\left|{F}\right|-1\right)\subseteq \left(0..^\left|{F}\right|\right)$
42 41 adantl ${⊢}\left({F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{E}\wedge \left|{F}\right|\in {ℕ}_{0}\right)\to \left(0..^\left|{F}\right|-1\right)\subseteq \left(0..^\left|{F}\right|\right)$
43 42 sselda ${⊢}\left(\left({F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{E}\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge {i}\in \left(0..^\left|{F}\right|-1\right)\right)\to {i}\in \left(0..^\left|{F}\right|\right)$
44 39 43 ffvelrnd ${⊢}\left(\left({F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{E}\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge {i}\in \left(0..^\left|{F}\right|-1\right)\right)\to {F}\left({i}\right)\in \mathrm{dom}{E}$
45 44 exp31 ${⊢}{F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{E}\to \left(\left|{F}\right|\in {ℕ}_{0}\to \left({i}\in \left(0..^\left|{F}\right|-1\right)\to {F}\left({i}\right)\in \mathrm{dom}{E}\right)\right)$
46 38 45 syl ${⊢}{F}\in \mathrm{Word}\mathrm{dom}{E}\to \left(\left|{F}\right|\in {ℕ}_{0}\to \left({i}\in \left(0..^\left|{F}\right|-1\right)\to {F}\left({i}\right)\in \mathrm{dom}{E}\right)\right)$
47 46 adantl ${⊢}\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\to \left(\left|{F}\right|\in {ℕ}_{0}\to \left({i}\in \left(0..^\left|{F}\right|-1\right)\to {F}\left({i}\right)\in \mathrm{dom}{E}\right)\right)$
48 47 imp ${⊢}\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\to \left({i}\in \left(0..^\left|{F}\right|-1\right)\to {F}\left({i}\right)\in \mathrm{dom}{E}\right)$
49 48 ad3antrrr ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left({i}\in \left(0..^\left|{F}\right|-1\right)\to {F}\left({i}\right)\in \mathrm{dom}{E}\right)$
50 49 imp ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge {i}\in \left(0..^\left|{F}\right|-1\right)\right)\to {F}\left({i}\right)\in \mathrm{dom}{E}$
51 37 50 ffvelrnd ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge {i}\in \left(0..^\left|{F}\right|-1\right)\right)\to {E}\left({F}\left({i}\right)\right)\in \mathrm{ran}{E}$
52 eqcom ${⊢}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}↔\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}={E}\left({F}\left({i}\right)\right)$
53 52 biimpi ${⊢}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\to \left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}={E}\left({F}\left({i}\right)\right)$
54 53 eleq1d ${⊢}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\to \left(\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}↔{E}\left({F}\left({i}\right)\right)\in \mathrm{ran}{E}\right)$
55 51 54 syl5ibrcom ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge {i}\in \left(0..^\left|{F}\right|-1\right)\right)\to \left({E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\to \left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\right)$
56 55 ralimdva ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left(\forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\to \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\right)$
57 35 56 syldc ${⊢}\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\to \left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\right)$
58 57 adantr ${⊢}\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\right)$
59 58 impcom ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\right)\to \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}$
60 breq2 ${⊢}\left|{P}\right|=\left|{F}\right|+1\to \left(2\le \left|{P}\right|↔2\le \left|{F}\right|+1\right)$
61 60 adantl ${⊢}\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\to \left(2\le \left|{P}\right|↔2\le \left|{F}\right|+1\right)$
62 2re ${⊢}2\in ℝ$
63 62 a1i ${⊢}\left|{F}\right|\in {ℕ}_{0}\to 2\in ℝ$
64 1red ${⊢}\left|{F}\right|\in {ℕ}_{0}\to 1\in ℝ$
65 63 64 28 lesubaddd ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left(2-1\le \left|{F}\right|↔2\le \left|{F}\right|+1\right)$
66 2m1e1 ${⊢}2-1=1$
67 66 breq1i ${⊢}2-1\le \left|{F}\right|↔1\le \left|{F}\right|$
68 elnnnn0c ${⊢}\left|{F}\right|\in ℕ↔\left(\left|{F}\right|\in {ℕ}_{0}\wedge 1\le \left|{F}\right|\right)$
69 68 simplbi2 ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left(1\le \left|{F}\right|\to \left|{F}\right|\in ℕ\right)$
70 67 69 syl5bi ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left(2-1\le \left|{F}\right|\to \left|{F}\right|\in ℕ\right)$
71 65 70 sylbird ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left(2\le \left|{F}\right|+1\to \left|{F}\right|\in ℕ\right)$
72 71 adantl ${⊢}\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\to \left(2\le \left|{F}\right|+1\to \left|{F}\right|\in ℕ\right)$
73 72 adantr ${⊢}\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\to \left(2\le \left|{F}\right|+1\to \left|{F}\right|\in ℕ\right)$
74 61 73 sylbid ${⊢}\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\to \left(2\le \left|{P}\right|\to \left|{F}\right|\in ℕ\right)$
75 74 imp ${⊢}\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\to \left|{F}\right|\in ℕ$
76 75 adantr ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left|{F}\right|\in ℕ$
77 lbfzo0 ${⊢}0\in \left(0..^\left|{F}\right|\right)↔\left|{F}\right|\in ℕ$
78 76 77 sylibr ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to 0\in \left(0..^\left|{F}\right|\right)$
79 fzoend ${⊢}0\in \left(0..^\left|{F}\right|\right)\to \left|{F}\right|-1\in \left(0..^\left|{F}\right|\right)$
80 78 79 syl ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left|{F}\right|-1\in \left(0..^\left|{F}\right|\right)$
81 2fveq3 ${⊢}{i}=\left|{F}\right|-1\to {E}\left({F}\left({i}\right)\right)={E}\left({F}\left(\left|{F}\right|-1\right)\right)$
82 fveq2 ${⊢}{i}=\left|{F}\right|-1\to {P}\left({i}\right)={P}\left(\left|{F}\right|-1\right)$
83 fvoveq1 ${⊢}{i}=\left|{F}\right|-1\to {P}\left({i}+1\right)={P}\left(\left|{F}\right|-1+1\right)$
84 82 83 preq12d ${⊢}{i}=\left|{F}\right|-1\to \left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}=\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|-1+1\right)\right\}$
85 81 84 eqeq12d ${⊢}{i}=\left|{F}\right|-1\to \left({E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}↔{E}\left({F}\left(\left|{F}\right|-1\right)\right)=\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|-1+1\right)\right\}\right)$
86 85 adantl ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge {i}=\left|{F}\right|-1\right)\to \left({E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}↔{E}\left({F}\left(\left|{F}\right|-1\right)\right)=\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|-1+1\right)\right\}\right)$
87 80 86 rspcdv ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\to {E}\left({F}\left(\left|{F}\right|-1\right)\right)=\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|-1+1\right)\right\}\right)$
88 14 15 npcand ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left|{F}\right|-1+1=\left|{F}\right|$
89 88 ad4antlr ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left|{F}\right|-1+1=\left|{F}\right|$
90 89 fveq2d ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to {P}\left(\left|{F}\right|-1+1\right)={P}\left(\left|{F}\right|\right)$
91 90 preq2d ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|-1+1\right)\right\}=\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}$
92 91 eqeq2d ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left({E}\left({F}\left(\left|{F}\right|-1\right)\right)=\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|-1+1\right)\right\}↔{E}\left({F}\left(\left|{F}\right|-1\right)\right)=\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}\right)$
93 38 ad4antlr ${⊢}\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\to {F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{E}$
94 71 com12 ${⊢}2\le \left|{F}\right|+1\to \left(\left|{F}\right|\in {ℕ}_{0}\to \left|{F}\right|\in ℕ\right)$
95 60 94 syl6bi ${⊢}\left|{P}\right|=\left|{F}\right|+1\to \left(2\le \left|{P}\right|\to \left(\left|{F}\right|\in {ℕ}_{0}\to \left|{F}\right|\in ℕ\right)\right)$
96 95 com3r ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left(\left|{P}\right|=\left|{F}\right|+1\to \left(2\le \left|{P}\right|\to \left|{F}\right|\in ℕ\right)\right)$
97 96 adantl ${⊢}\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\to \left(\left|{P}\right|=\left|{F}\right|+1\to \left(2\le \left|{P}\right|\to \left|{F}\right|\in ℕ\right)\right)$
98 97 imp31 ${⊢}\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\to \left|{F}\right|\in ℕ$
99 98 77 sylibr ${⊢}\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\to 0\in \left(0..^\left|{F}\right|\right)$
100 99 79 syl ${⊢}\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\to \left|{F}\right|-1\in \left(0..^\left|{F}\right|\right)$
101 93 100 ffvelrnd ${⊢}\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\to {F}\left(\left|{F}\right|-1\right)\in \mathrm{dom}{E}$
102 101 adantr ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to {F}\left(\left|{F}\right|-1\right)\in \mathrm{dom}{E}$
103 36 102 ffvelrnd ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to {E}\left({F}\left(\left|{F}\right|-1\right)\right)\in \mathrm{ran}{E}$
104 eqcom ${⊢}{E}\left({F}\left(\left|{F}\right|-1\right)\right)=\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}↔\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}={E}\left({F}\left(\left|{F}\right|-1\right)\right)$
105 104 biimpi ${⊢}{E}\left({F}\left(\left|{F}\right|-1\right)\right)=\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}\to \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}={E}\left({F}\left(\left|{F}\right|-1\right)\right)$
106 105 eleq1d ${⊢}{E}\left({F}\left(\left|{F}\right|-1\right)\right)=\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}\to \left(\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}\in \mathrm{ran}{E}↔{E}\left({F}\left(\left|{F}\right|-1\right)\right)\in \mathrm{ran}{E}\right)$
107 103 106 syl5ibrcom ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left({E}\left({F}\left(\left|{F}\right|-1\right)\right)=\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}\to \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}\in \mathrm{ran}{E}\right)$
108 92 107 sylbid ${⊢}\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left({E}\left({F}\left(\left|{F}\right|-1\right)\right)=\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|-1+1\right)\right\}\to \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}\in \mathrm{ran}{E}\right)$
109 87 108 syldc ${⊢}\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\to \left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}\in \mathrm{ran}{E}\right)$
110 109 adantr ${⊢}\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\to \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}\in \mathrm{ran}{E}\right)$
111 110 impcom ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\right)\to \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}\in \mathrm{ran}{E}$
112 preq2 ${⊢}{P}\left(0\right)={P}\left(\left|{F}\right|\right)\to \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}=\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}$
113 112 eleq1d ${⊢}{P}\left(0\right)={P}\left(\left|{F}\right|\right)\to \left(\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}↔\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}\in \mathrm{ran}{E}\right)$
114 113 adantl ${⊢}\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}↔\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}\in \mathrm{ran}{E}\right)$
115 114 adantl ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\right)\to \left(\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}↔\left\{{P}\left(\left|{F}\right|-1\right),{P}\left(\left|{F}\right|\right)\right\}\in \mathrm{ran}{E}\right)$
116 111 115 mpbird ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\right)\to \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}$
117 24 59 116 3jca ${⊢}\left(\left(\left(\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\wedge 2\le \left|{P}\right|\right)\wedge {E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\right)\wedge \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)$
118 117 exp41 ${⊢}\left(\left(\left({P}\in \mathrm{Word}{V}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left|{F}\right|\in {ℕ}_{0}\right)\wedge \left|{P}\right|=\left|{F}\right|+1\right)\to \left(2\le \left|{P}\right|\to \left({E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\to \left(\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)\right)\right)\right)$
119 118 exp41 ${⊢}{P}\in \mathrm{Word}{V}\to \left({F}\in \mathrm{Word}\mathrm{dom}{E}\to \left(\left|{F}\right|\in {ℕ}_{0}\to \left(\left|{P}\right|=\left|{F}\right|+1\to \left(2\le \left|{P}\right|\to \left({E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\to \left(\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)\right)\right)\right)\right)\right)\right)$
120 8 119 syl ${⊢}{P}:\left(0\dots \left|{F}\right|\right)⟶{V}\to \left({F}\in \mathrm{Word}\mathrm{dom}{E}\to \left(\left|{F}\right|\in {ℕ}_{0}\to \left(\left|{P}\right|=\left|{F}\right|+1\to \left(2\le \left|{P}\right|\to \left({E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\to \left(\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)\right)\right)\right)\right)\right)\right)$
121 120 com13 ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left({F}\in \mathrm{Word}\mathrm{dom}{E}\to \left({P}:\left(0\dots \left|{F}\right|\right)⟶{V}\to \left(\left|{P}\right|=\left|{F}\right|+1\to \left(2\le \left|{P}\right|\to \left({E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\to \left(\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)\right)\right)\right)\right)\right)\right)$
122 4 121 mpcom ${⊢}{F}\in \mathrm{Word}\mathrm{dom}{E}\to \left({P}:\left(0\dots \left|{F}\right|\right)⟶{V}\to \left(\left|{P}\right|=\left|{F}\right|+1\to \left(2\le \left|{P}\right|\to \left({E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\to \left(\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)\right)\right)\right)\right)\right)$
123 122 imp ${⊢}\left({F}\in \mathrm{Word}\mathrm{dom}{E}\wedge {P}:\left(0\dots \left|{F}\right|\right)⟶{V}\right)\to \left(\left|{P}\right|=\left|{F}\right|+1\to \left(2\le \left|{P}\right|\to \left({E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\to \left(\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)\right)\right)\right)\right)$
124 7 123 mpd ${⊢}\left({F}\in \mathrm{Word}\mathrm{dom}{E}\wedge {P}:\left(0\dots \left|{F}\right|\right)⟶{V}\right)\to \left(2\le \left|{P}\right|\to \left({E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\to \left(\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)\right)\right)\right)$
125 124 expcom ${⊢}{P}:\left(0\dots \left|{F}\right|\right)⟶{V}\to \left({F}\in \mathrm{Word}\mathrm{dom}{E}\to \left(2\le \left|{P}\right|\to \left({E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\to \left(\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)\right)\right)\right)\right)$
126 125 com14 ${⊢}{E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\to \left({F}\in \mathrm{Word}\mathrm{dom}{E}\to \left(2\le \left|{P}\right|\to \left({P}:\left(0\dots \left|{F}\right|\right)⟶{V}\to \left(\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)\right)\right)\right)\right)$
127 126 imp ${⊢}\left({E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\to \left(2\le \left|{P}\right|\to \left({P}:\left(0\dots \left|{F}\right|\right)⟶{V}\to \left(\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)\right)\right)\right)$
128 127 impcomd ${⊢}\left({E}:\mathrm{dom}{E}⟶\mathrm{ran}{E}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\to \left(\left({P}:\left(0\dots \left|{F}\right|\right)⟶{V}\wedge 2\le \left|{P}\right|\right)\to \left(\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)\right)\right)$
129 3 128 sylan ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\to \left(\left({P}:\left(0\dots \left|{F}\right|\right)⟶{V}\wedge 2\le \left|{P}\right|\right)\to \left(\left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)\right)\right)$
130 129 3imp ${⊢}\left(\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}{R}\wedge {F}\in \mathrm{Word}\mathrm{dom}{E}\right)\wedge \left({P}:\left(0\dots \left|{F}\right|\right)⟶{V}\wedge 2\le \left|{P}\right|\right)\wedge \left(\forall {i}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{E}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\right)\to \left(\mathrm{lastS}\left({P}\right)={P}\left(0\right)\wedge \forall {i}\in \left(0..^\left|{F}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\in \mathrm{ran}{E}\wedge \left\{{P}\left(\left|{F}\right|-1\right),{P}\left(0\right)\right\}\in \mathrm{ran}{E}\right)$