Metamath Proof Explorer

Theorem clwlkclwwlklem3

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

Ref Expression
Assertion clwlkclwwlklem3 ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∃ 𝑓 ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐸 : dom 𝐸 –1-1→ 𝑅 )
2 simp1 ⊢ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → 𝑓 ∈ Word dom 𝐸 )
3 2 adantr ⊢ ( ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) → 𝑓 ∈ Word dom 𝐸 )
4 1 3 anim12i ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) → ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑓 ∈ Word dom 𝐸 ) )
5 simp3 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
6 simpl2 ⊢ ( ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 )
7 5 6 anim12ci ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) )
8 simp3 ⊢ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } )
9 8 anim1i ⊢ ( ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) )
10 9 adantl ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) )
11 clwlkclwwlklem2 ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑓 ∈ Word dom 𝐸 ) ∧ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) )
12 4 7 10 11 syl3anc ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) )
13 lencl ⊢ ( 𝑃 ∈ Word 𝑉 → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
14 lencl ⊢ ( 𝑓 ∈ Word dom 𝐸 → ( ♯ ‘ 𝑓 ) ∈ ℕ0 )
15 ffz0hash ⊢ ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ) → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) )
16 oveq1 ⊢ ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ( ( ♯ ‘ 𝑓 ) + 1 ) − 1 ) )
17 16 oveq1d ⊢ ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) → ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) = ( ( ( ( ♯ ‘ 𝑓 ) + 1 ) − 1 ) − 0 ) )
18 nn0cn ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( ♯ ‘ 𝑓 ) ∈ ℂ )
19 peano2cn ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℂ → ( ( ♯ ‘ 𝑓 ) + 1 ) ∈ ℂ )
20 peano2cnm ⊢ ( ( ( ♯ ‘ 𝑓 ) + 1 ) ∈ ℂ → ( ( ( ♯ ‘ 𝑓 ) + 1 ) − 1 ) ∈ ℂ )
21 18 19 20 3syl ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝑓 ) + 1 ) − 1 ) ∈ ℂ )
22 21 subid1d ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( ( ( ( ♯ ‘ 𝑓 ) + 1 ) − 1 ) − 0 ) = ( ( ( ♯ ‘ 𝑓 ) + 1 ) − 1 ) )
23 1cnd ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → 1 ∈ ℂ )
24 18 23 pncand ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝑓 ) + 1 ) − 1 ) = ( ♯ ‘ 𝑓 ) )
25 22 24 eqtrd ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( ( ( ( ♯ ‘ 𝑓 ) + 1 ) − 1 ) − 0 ) = ( ♯ ‘ 𝑓 ) )
26 25 adantr ⊢ ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( ( ( ( ♯ ‘ 𝑓 ) + 1 ) − 1 ) − 0 ) = ( ♯ ‘ 𝑓 ) )
27 17 26 sylan9eqr ⊢ ( ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) → ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) = ( ♯ ‘ 𝑓 ) )
28 27 oveq1d ⊢ ( ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) = ( ( ♯ ‘ 𝑓 ) − 1 ) )
29 28 oveq2d ⊢ ( ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) → ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) )
30 29 raleqdv ⊢ ( ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
31 oveq1 ⊢ ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) → ( ( ♯ ‘ 𝑃 ) − 2 ) = ( ( ( ♯ ‘ 𝑓 ) + 1 ) − 2 ) )
32 2cnd ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → 2 ∈ ℂ )
33 18 32 23 subsub3d ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑓 ) − ( 2 − 1 ) ) = ( ( ( ♯ ‘ 𝑓 ) + 1 ) − 2 ) )
34 2m1e1 ⊢ ( 2 − 1 ) = 1
35 34 a1i ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( 2 − 1 ) = 1 )
36 35 oveq2d ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑓 ) − ( 2 − 1 ) ) = ( ( ♯ ‘ 𝑓 ) − 1 ) )
37 33 36 eqtr3d ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝑓 ) + 1 ) − 2 ) = ( ( ♯ ‘ 𝑓 ) − 1 ) )
38 37 adantr ⊢ ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( ( ( ♯ ‘ 𝑓 ) + 1 ) − 2 ) = ( ( ♯ ‘ 𝑓 ) − 1 ) )
39 31 38 sylan9eqr ⊢ ( ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) = ( ( ♯ ‘ 𝑓 ) − 1 ) )
40 39 fveq2d ⊢ ( ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) → ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) )
41 40 preq1d ⊢ ( ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } )
42 41 eleq1d ⊢ ( ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) )
43 30 42 anbi12d ⊢ ( ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) )
44 43 anbi2d ⊢ ( ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
45 3anass ⊢ ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) )
46 44 45 bitr4di ⊢ ( ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) )
47 46 expcom ⊢ ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) → ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
48 47 expd ⊢ ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) → ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) )
49 15 48 syl ⊢ ( ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ) → ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) )
50 49 ex ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 → ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) ) )
51 50 com23 ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) ) )
52 14 14 51 sylc ⊢ ( 𝑓 ∈ Word dom 𝐸 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ) )
53 52 imp ⊢ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
54 53 3adant3 ⊢ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
55 54 adantr ⊢ ( ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
56 13 55 syl5com ⊢ ( 𝑃 ∈ Word 𝑉 → ( ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
57 56 3ad2ant2 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
58 57 imp ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑓 ) − 1 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) )
59 12 58 mpbird ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) )
60 59 ex ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
61 60 exlimdv ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∃ 𝑓 ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) → ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
62 clwlkclwwlklem1 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ∃ 𝑓 ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) )
63 61 62 impbid ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∃ 𝑓 ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )