Metamath Proof Explorer

Theorem clwlkclwwlklem2a

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

Ref Expression
Hypothesis clwlkclwwlklem2.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
Assertion clwlkclwwlklem2a ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( 𝐹 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlklem2.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
2 simpl ⊢ ( ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) )
3 f1f1orn ⊢ ( 𝐸 : dom 𝐸 –1-1→ 𝑅 → 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 )
4 3 3ad2ant1 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 )
5 4 adantr ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 )
6 5 ad2antrl ⊢ ( ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 )
7 elfzo0 ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
8 lencl ⊢ ( 𝑃 ∈ Word 𝑉 → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
9 simpl ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
10 9 adantr ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ) → 𝑥 ∈ ℕ0 )
11 elnn0z ⊢ ( 𝑥 ∈ ℕ0 ↔ ( 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥 ) )
12 0red ⊢ ( ( 𝑥 ∈ ℤ ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → 0 ∈ ℝ )
13 zre ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
14 13 adantr ⊢ ( ( 𝑥 ∈ ℤ ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → 𝑥 ∈ ℝ )
15 nn0re ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℝ )
16 2re ⊢ 2 ∈ ℝ
17 16 a1i ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 2 ∈ ℝ )
18 15 17 resubcld ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ )
19 18 adantl ⊢ ( ( 𝑥 ∈ ℤ ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ )
20 lelttr ⊢ ( ( 0 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ ) → ( ( 0 ≤ 𝑥 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → 0 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
21 12 14 19 20 syl3anc ⊢ ( ( 𝑥 ∈ ℤ ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( ( 0 ≤ 𝑥 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → 0 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
22 nn0z ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℤ )
23 2z ⊢ 2 ∈ ℤ
24 23 a1i ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 2 ∈ ℤ )
25 22 24 zsubcld ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ )
26 25 anim1i ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 0 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ ∧ 0 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
27 elnnz ⊢ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℕ ↔ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ ∧ 0 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
28 26 27 sylibr ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 0 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℕ )
29 nn0cn ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℂ )
30 peano2cnm ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℂ → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℂ )
31 29 30 syl ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℂ )
32 31 subid1d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
33 32 oveq1d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) = ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) )
34 1cnd ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 1 ∈ ℂ )
35 29 34 34 subsub4d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝑃 ) − ( 1 + 1 ) ) )
36 1p1e2 ⊢ ( 1 + 1 ) = 2
37 36 a1i ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 1 + 1 ) = 2 )
38 37 oveq2d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − ( 1 + 1 ) ) = ( ( ♯ ‘ 𝑃 ) − 2 ) )
39 35 38 eqtrd ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝑃 ) − 2 ) )
40 33 39 eqtrd ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) = ( ( ♯ ‘ 𝑃 ) − 2 ) )
41 40 eleq1d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℕ ) )
42 41 adantr ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 0 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℕ ) )
43 28 42 mpbird ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 0 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ )
44 43 ex ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 0 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ ) )
45 44 adantl ⊢ ( ( 𝑥 ∈ ℤ ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 0 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ ) )
46 21 45 syld ⊢ ( ( 𝑥 ∈ ℤ ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( ( 0 ≤ 𝑥 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ ) )
47 46 exp4b ⊢ ( 𝑥 ∈ ℤ → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 0 ≤ 𝑥 → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ ) ) ) )
48 47 com23 ⊢ ( 𝑥 ∈ ℤ → ( 0 ≤ 𝑥 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ ) ) ) )
49 48 imp ⊢ ( ( 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥 ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ ) ) )
50 11 49 sylbi ⊢ ( 𝑥 ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ ) ) )
51 50 imp ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ ) )
52 51 com12 ⊢ ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ ) )
53 52 adantr ⊢ ( ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ ) )
54 53 impcom ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ) → ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ )
55 df-2 ⊢ 2 = ( 1 + 1 )
56 55 a1i ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 2 = ( 1 + 1 ) )
57 56 oveq2d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) = ( ( ♯ ‘ 𝑃 ) − ( 1 + 1 ) ) )
58 32 eqcomd ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) )
59 58 oveq1d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) = ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) )
60 57 35 59 3eqtr2d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) = ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) )
61 60 adantl ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑃 ) − 2 ) = ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) )
62 61 breq2d ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ↔ 𝑥 < ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) )
63 62 biimpcd ⊢ ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → 𝑥 < ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) )
64 63 adantr ⊢ ( ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → 𝑥 < ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) )
65 64 impcom ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ) → 𝑥 < ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) )
66 elfzo0 ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ∈ ℕ ∧ 𝑥 < ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) )
67 10 54 65 66 syl3anbrc ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) )
68 67 exp32 ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ) ) )
69 68 a1d ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ) ) ) )
70 69 com24 ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ) ) ) )
71 70 ex ⊢ ( 𝑥 ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ) ) ) ) )
72 71 com25 ⊢ ( 𝑥 ∈ ℕ0 → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ) ) ) ) )
73 72 imp ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ) ) ) )
74 73 3adant2 ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ) ) ) )
75 74 com14 ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( 𝑥 ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ) ) ) )
76 8 75 syl ⊢ ( 𝑃 ∈ Word 𝑉 → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( 𝑥 ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ) ) ) )
77 76 imp ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( 𝑥 ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ) ) )
78 77 3adant1 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( 𝑥 ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ) ) )
79 7 78 syl7bi ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ) ) )
80 79 com13 ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) ) ) )
81 80 imp31 ⊢ ( ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) ∧ ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) )
82 fveq2 ⊢ ( 𝑖 = 𝑥 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑥 ) )
83 fvoveq1 ⊢ ( 𝑖 = 𝑥 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) )
84 82 83 preq12d ⊢ ( 𝑖 = 𝑥 → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } )
85 84 eleq1d ⊢ ( 𝑖 = 𝑥 → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) )
86 85 adantl ⊢ ( ( ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) ∧ ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ) ∧ 𝑖 = 𝑥 ) → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) )
87 81 86 rspcdv ⊢ ( ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) ∧ ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) )
88 87 ex ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) ) )
89 88 com13 ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) ) )
90 89 ad2antrl ⊢ ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) ) )
91 90 impcom ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) )
92 91 expdimp ⊢ ( ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) )
93 92 impcom ⊢ ( ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 )
94 f1ocnvdm ⊢ ( ( 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 ∧ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ dom 𝐸 )
95 6 93 94 syl2anc ⊢ ( ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ dom 𝐸 )
96 2 95 jca ⊢ ( ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ dom 𝐸 ) )
97 96 orcd ⊢ ( ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → ( ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ dom 𝐸 ) ∨ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ∈ dom 𝐸 ) ) )
98 simpl ⊢ ( ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) )
99 5 ad2antrl ⊢ ( ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 )
100 nn0z ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℤ )
101 peano2zm ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℤ → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ )
102 22 101 syl ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ )
103 100 102 anim12i ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 𝑥 ∈ ℤ ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ ) )
104 zltlem1 ⊢ ( ( 𝑥 ∈ ℤ ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ↔ 𝑥 ≤ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) )
105 103 104 syl ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ↔ 𝑥 ≤ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) )
106 39 adantl ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝑃 ) − 2 ) )
107 106 breq2d ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 𝑥 ≤ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ↔ 𝑥 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
108 107 biimpd ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 𝑥 ≤ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) → 𝑥 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
109 105 108 sylbid ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) → 𝑥 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
110 109 impancom ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 𝑥 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
111 110 imp ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → 𝑥 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) )
112 nn0re ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℝ )
113 112 adantr ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → 𝑥 ∈ ℝ )
114 113 18 anim12i ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 𝑥 ∈ ℝ ∧ ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ ) )
115 lenlt ⊢ ( ( 𝑥 ∈ ℝ ∧ ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ ) → ( 𝑥 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ↔ ¬ ( ( ♯ ‘ 𝑃 ) − 2 ) < 𝑥 ) )
116 114 115 syl ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 𝑥 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ↔ ¬ ( ( ♯ ‘ 𝑃 ) − 2 ) < 𝑥 ) )
117 111 116 mpbid ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ¬ ( ( ♯ ‘ 𝑃 ) − 2 ) < 𝑥 )
118 117 anim1i ⊢ ( ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ¬ ( ( ♯ ‘ 𝑃 ) − 2 ) < 𝑥 ∧ ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
119 114 ancomd ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) )
120 119 adantr ⊢ ( ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) )
121 lttri3 ⊢ ( ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ♯ ‘ 𝑃 ) − 2 ) = 𝑥 ↔ ( ¬ ( ( ♯ ‘ 𝑃 ) − 2 ) < 𝑥 ∧ ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) )
122 120 121 syl ⊢ ( ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ( ( ♯ ‘ 𝑃 ) − 2 ) = 𝑥 ↔ ( ¬ ( ( ♯ ‘ 𝑃 ) − 2 ) < 𝑥 ∧ ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) )
123 118 122 mpbird ⊢ ( ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) ∧ ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) = 𝑥 )
124 123 exp31 ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ♯ ‘ 𝑃 ) − 2 ) = 𝑥 ) ) )
125 124 com23 ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) = 𝑥 ) ) )
126 125 3adant2 ⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ ∧ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) = 𝑥 ) ) )
127 7 126 sylbi ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) = 𝑥 ) ) )
128 127 impcom ⊢ ( ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) = 𝑥 ) )
129 8 128 syl5com ⊢ ( 𝑃 ∈ Word 𝑉 → ( ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) = 𝑥 ) )
130 129 3ad2ant2 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) = 𝑥 ) )
131 130 imp ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) = 𝑥 )
132 131 fveq2d ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) = ( 𝑃 ‘ 𝑥 ) )
133 132 preq1d ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } )
134 133 eleq1d ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) )
135 134 biimpd ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) )
136 135 exp32 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
137 136 com12 ⊢ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
138 137 com14 ⊢ ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 → ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
139 138 adantl ⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) → ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
140 139 adantl ⊢ ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
141 140 com12 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
142 141 imp31 ⊢ ( ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) )
143 142 impcom ⊢ ( ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 )
144 f1ocnvdm ⊢ ( ( 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 ∧ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ∈ dom 𝐸 )
145 99 143 144 syl2anc ⊢ ( ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ∈ dom 𝐸 )
146 98 145 jca ⊢ ( ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ∈ dom 𝐸 ) )
147 146 olcd ⊢ ( ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ) → ( ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ dom 𝐸 ) ∨ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ∈ dom 𝐸 ) ) )
148 97 147 pm2.61ian ⊢ ( ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ dom 𝐸 ) ∨ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ∈ dom 𝐸 ) ) )
149 ifel ⊢ ( if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ∈ dom 𝐸 ↔ ( ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ dom 𝐸 ) ∨ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ∈ dom 𝐸 ) ) )
150 148 149 sylibr ⊢ ( ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ∈ dom 𝐸 )
151 150 1 fmptd ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → 𝐹 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom 𝐸 )
152 iswrdi ⊢ ( 𝐹 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom 𝐸 → 𝐹 ∈ Word dom 𝐸 )
153 151 152 syl ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → 𝐹 ∈ Word dom 𝐸 )
154 wrdf ⊢ ( 𝑃 ∈ Word 𝑉 → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ 𝑉 )
155 154 adantr ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ 𝑉 )
156 1 clwlkclwwlklem2a2 ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
157 fzoval ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
158 8 22 157 3syl ⊢ ( 𝑃 ∈ Word 𝑉 → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
159 oveq2 ⊢ ( ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝐹 ) → ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
160 159 eqcoms ⊢ ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
161 158 160 sylan9eq ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
162 156 161 syldan ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
163 162 feq2d ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
164 155 163 mpbid ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
165 164 3adant1 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
166 165 adantr ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
167 clwlkclwwlklem2a1 ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
168 167 3adant1 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
169 168 imp ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 )
170 156 3adant1 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
171 170 adantr ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ) → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
172 1 clwlkclwwlklem2a4 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
173 172 impl ⊢ ( ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
174 173 ralimdva ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
175 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
176 175 raleqdv ⊢ ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
177 176 imbi2d ⊢ ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
178 174 177 imbitrrid ⊢ ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
179 171 178 mpcom ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
180 179 adantrr ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
181 169 180 mpd ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } )
182 153 166 181 3jca ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ( 𝐹 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
183 1 clwlkclwwlklem2a3 ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( lastS ‘ 𝑃 ) )
184 183 3adant1 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( lastS ‘ 𝑃 ) )
185 184 eqcomd ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
186 185 eqeq2d ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( 𝑃 ‘ 0 ) = ( lastS ‘ 𝑃 ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
187 186 biimpcd ⊢ ( ( 𝑃 ‘ 0 ) = ( lastS ‘ 𝑃 ) → ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
188 187 eqcoms ⊢ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) → ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
189 188 adantr ⊢ ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
190 189 impcom ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
191 182 190 jca ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) → ( ( 𝐹 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
192 191 ex ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ 𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) → ( ( 𝐹 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐸 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )