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 ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝐹 ∈ Word dom 𝐸 ) ∧ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) )

Proof

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