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 syl5ibr ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 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 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )