Metamath Proof Explorer

Theorem numclwwlk1lem2f1

Description: T is a 1-1 function. (Contributed by AV, 26-Sep-2018) (Revised by AV, 29-May-2021) (Proof shortened by AV, 23-Feb-2022) (Revised by AV, 31-Oct-2022)

Ref Expression
Hypotheses extwwlkfab.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
extwwlkfab.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
extwwlkfab.f ⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
numclwwlk.t ⊢ 𝑇 = ( 𝑢 ∈ ( 𝑋 𝐶 𝑁 ) ↦ ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ )
Assertion numclwwlk1lem2f1 ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑇 : ( 𝑋 𝐶 𝑁 ) –1-1→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 extwwlkfab.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 extwwlkfab.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
3 extwwlkfab.f ⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
4 numclwwlk.t ⊢ 𝑇 = ( 𝑢 ∈ ( 𝑋 𝐶 𝑁 ) ↦ ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ )
5 1 2 3 4 numclwwlk1lem2f ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑇 : ( 𝑋 𝐶 𝑁 ) ⟶ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )
6 1 2 3 4 numclwwlk1lem2fv ⊢ ( 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) → ( 𝑇 ‘ 𝑝 ) = ⟨ ( 𝑝 prefix ( 𝑁 − 2 ) ) , ( 𝑝 ‘ ( 𝑁 − 1 ) ) ⟩ )
7 6 ad2antrl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ∧ 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ) ) → ( 𝑇 ‘ 𝑝 ) = ⟨ ( 𝑝 prefix ( 𝑁 − 2 ) ) , ( 𝑝 ‘ ( 𝑁 − 1 ) ) ⟩ )
8 1 2 3 4 numclwwlk1lem2fv ⊢ ( 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) → ( 𝑇 ‘ 𝑎 ) = ⟨ ( 𝑎 prefix ( 𝑁 − 2 ) ) , ( 𝑎 ‘ ( 𝑁 − 1 ) ) ⟩ )
9 8 ad2antll ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ∧ 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ) ) → ( 𝑇 ‘ 𝑎 ) = ⟨ ( 𝑎 prefix ( 𝑁 − 2 ) ) , ( 𝑎 ‘ ( 𝑁 − 1 ) ) ⟩ )
10 7 9 eqeq12d ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ∧ 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ) ) → ( ( 𝑇 ‘ 𝑝 ) = ( 𝑇 ‘ 𝑎 ) ↔ ⟨ ( 𝑝 prefix ( 𝑁 − 2 ) ) , ( 𝑝 ‘ ( 𝑁 − 1 ) ) ⟩ = ⟨ ( 𝑎 prefix ( 𝑁 − 2 ) ) , ( 𝑎 ‘ ( 𝑁 − 1 ) ) ⟩ ) )
11 ovex ⊢ ( 𝑝 prefix ( 𝑁 − 2 ) ) ∈ V
12 fvex ⊢ ( 𝑝 ‘ ( 𝑁 − 1 ) ) ∈ V
13 11 12 opth ⊢ ( ⟨ ( 𝑝 prefix ( 𝑁 − 2 ) ) , ( 𝑝 ‘ ( 𝑁 − 1 ) ) ⟩ = ⟨ ( 𝑎 prefix ( 𝑁 − 2 ) ) , ( 𝑎 ‘ ( 𝑁 − 1 ) ) ⟩ ↔ ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) )
14 uzuzle23 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
15 2 2clwwlkel ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( 𝑝 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
16 isclwwlknon ⊢ ( 𝑝 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) )
17 16 anbi1i ⊢ ( ( 𝑝 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
18 15 17 bitrdi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
19 2 2clwwlkel ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
20 isclwwlknon ⊢ ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) )
21 20 anbi1i ⊢ ( ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
22 19 21 bitrdi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
23 18 22 anbi12d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ∧ 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ) ↔ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )
24 14 23 sylan2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ∧ 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ) ↔ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )
25 24 3adant1 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ∧ 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ) ↔ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )
26 1 clwwlknbp ⊢ ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) )
27 26 adantr ⊢ ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) → ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) )
28 27 adantr ⊢ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) )
29 simpr ⊢ ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) → ( 𝑝 ‘ 0 ) = 𝑋 )
30 29 adantr ⊢ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑝 ‘ 0 ) = 𝑋 )
31 simpr ⊢ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 )
32 29 eqcomd ⊢ ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) → 𝑋 = ( 𝑝 ‘ 0 ) )
33 32 adantr ⊢ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → 𝑋 = ( 𝑝 ‘ 0 ) )
34 31 33 eqtrd ⊢ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑝 ‘ ( 𝑁 − 2 ) ) = ( 𝑝 ‘ 0 ) )
35 28 30 34 jca32 ⊢ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ( ( 𝑝 ‘ 0 ) = 𝑋 ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = ( 𝑝 ‘ 0 ) ) ) )
36 1 clwwlknbp ⊢ ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = 𝑁 ) )
37 36 adantr ⊢ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) → ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = 𝑁 ) )
38 37 adantr ⊢ ( ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = 𝑁 ) )
39 simpr ⊢ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) → ( 𝑎 ‘ 0 ) = 𝑋 )
40 39 adantr ⊢ ( ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑎 ‘ 0 ) = 𝑋 )
41 simpr ⊢ ( ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 )
42 39 eqcomd ⊢ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) → 𝑋 = ( 𝑎 ‘ 0 ) )
43 42 adantr ⊢ ( ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → 𝑋 = ( 𝑎 ‘ 0 ) )
44 41 43 eqtrd ⊢ ( ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑎 ‘ ( 𝑁 − 2 ) ) = ( 𝑎 ‘ 0 ) )
45 38 40 44 jca32 ⊢ ( ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = 𝑁 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑋 ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = ( 𝑎 ‘ 0 ) ) ) )
46 eqtr3 ⊢ ( ( ( ♯ ‘ 𝑝 ) = 𝑁 ∧ ( ♯ ‘ 𝑎 ) = 𝑁 ) → ( ♯ ‘ 𝑝 ) = ( ♯ ‘ 𝑎 ) )
47 46 expcom ⊢ ( ( ♯ ‘ 𝑎 ) = 𝑁 → ( ( ♯ ‘ 𝑝 ) = 𝑁 → ( ♯ ‘ 𝑝 ) = ( ♯ ‘ 𝑎 ) ) )
48 47 ad2antlr ⊢ ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = 𝑁 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑋 ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = ( 𝑎 ‘ 0 ) ) ) → ( ( ♯ ‘ 𝑝 ) = 𝑁 → ( ♯ ‘ 𝑝 ) = ( ♯ ‘ 𝑎 ) ) )
49 48 com12 ⊢ ( ( ♯ ‘ 𝑝 ) = 𝑁 → ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = 𝑁 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑋 ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = ( 𝑎 ‘ 0 ) ) ) → ( ♯ ‘ 𝑝 ) = ( ♯ ‘ 𝑎 ) ) )
50 49 ad2antlr ⊢ ( ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ( ( 𝑝 ‘ 0 ) = 𝑋 ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = ( 𝑝 ‘ 0 ) ) ) → ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = 𝑁 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑋 ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = ( 𝑎 ‘ 0 ) ) ) → ( ♯ ‘ 𝑝 ) = ( ♯ ‘ 𝑎 ) ) )
51 50 imp ⊢ ( ( ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ( ( 𝑝 ‘ 0 ) = 𝑋 ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = ( 𝑝 ‘ 0 ) ) ) ∧ ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = 𝑁 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑋 ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = ( 𝑎 ‘ 0 ) ) ) ) → ( ♯ ‘ 𝑝 ) = ( ♯ ‘ 𝑎 ) )
52 35 45 51 syl2an ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( ♯ ‘ 𝑝 ) = ( ♯ ‘ 𝑎 ) )
53 52 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ∧ ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) ) → ( ♯ ‘ 𝑝 ) = ( ♯ ‘ 𝑎 ) )
54 27 simprd ⊢ ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) → ( ♯ ‘ 𝑝 ) = 𝑁 )
55 54 adantr ⊢ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( ♯ ‘ 𝑝 ) = 𝑁 )
56 55 eqcomd ⊢ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → 𝑁 = ( ♯ ‘ 𝑝 ) )
57 56 adantr ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → 𝑁 = ( ♯ ‘ 𝑝 ) )
58 57 oveq1d ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑁 − 2 ) = ( ( ♯ ‘ 𝑝 ) − 2 ) )
59 58 oveq2d ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑝 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) )
60 58 oveq2d ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑎 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) )
61 59 60 eqeq12d ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ↔ ( 𝑝 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) ) )
62 61 biimpcd ⊢ ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) → ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑝 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) ) )
63 62 adantr ⊢ ( ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) → ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑝 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) ) )
64 63 impcom ⊢ ( ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ∧ ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) ) → ( 𝑝 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) )
65 55 oveq1d ⊢ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( ( ♯ ‘ 𝑝 ) − 2 ) = ( 𝑁 − 2 ) )
66 65 fveq2d ⊢ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑝 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑝 ‘ ( 𝑁 − 2 ) ) )
67 66 31 eqtrd ⊢ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑝 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) = 𝑋 )
68 67 adantr ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑝 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) = 𝑋 )
69 41 eqcomd ⊢ ( ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → 𝑋 = ( 𝑎 ‘ ( 𝑁 − 2 ) ) )
70 69 adantl ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → 𝑋 = ( 𝑎 ‘ ( 𝑁 − 2 ) ) )
71 58 fveq2d ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑎 ‘ ( 𝑁 − 2 ) ) = ( 𝑎 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) )
72 70 71 eqtrd ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → 𝑋 = ( 𝑎 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) )
73 68 72 eqtrd ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑝 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) )
74 73 adantr ⊢ ( ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ∧ ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) ) → ( 𝑝 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) )
75 lsw ⊢ ( 𝑝 ∈ Word 𝑉 → ( lastS ‘ 𝑝 ) = ( 𝑝 ‘ ( ( ♯ ‘ 𝑝 ) − 1 ) ) )
76 fvoveq1 ⊢ ( ( ♯ ‘ 𝑝 ) = 𝑁 → ( 𝑝 ‘ ( ( ♯ ‘ 𝑝 ) − 1 ) ) = ( 𝑝 ‘ ( 𝑁 − 1 ) ) )
77 75 76 sylan9eq ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) → ( lastS ‘ 𝑝 ) = ( 𝑝 ‘ ( 𝑁 − 1 ) ) )
78 26 77 syl ⊢ ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( lastS ‘ 𝑝 ) = ( 𝑝 ‘ ( 𝑁 − 1 ) ) )
79 78 eqcomd ⊢ ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( lastS ‘ 𝑝 ) )
80 79 ad3antrrr ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( lastS ‘ 𝑝 ) )
81 lsw ⊢ ( 𝑎 ∈ Word 𝑉 → ( lastS ‘ 𝑎 ) = ( 𝑎 ‘ ( ( ♯ ‘ 𝑎 ) − 1 ) ) )
82 81 adantr ⊢ ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = 𝑁 ) → ( lastS ‘ 𝑎 ) = ( 𝑎 ‘ ( ( ♯ ‘ 𝑎 ) − 1 ) ) )
83 oveq1 ⊢ ( 𝑁 = ( ♯ ‘ 𝑎 ) → ( 𝑁 − 1 ) = ( ( ♯ ‘ 𝑎 ) − 1 ) )
84 83 eqcoms ⊢ ( ( ♯ ‘ 𝑎 ) = 𝑁 → ( 𝑁 − 1 ) = ( ( ♯ ‘ 𝑎 ) − 1 ) )
85 84 fveq2d ⊢ ( ( ♯ ‘ 𝑎 ) = 𝑁 → ( 𝑎 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( ( ♯ ‘ 𝑎 ) − 1 ) ) )
86 85 eqeq2d ⊢ ( ( ♯ ‘ 𝑎 ) = 𝑁 → ( ( lastS ‘ 𝑎 ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ↔ ( lastS ‘ 𝑎 ) = ( 𝑎 ‘ ( ( ♯ ‘ 𝑎 ) − 1 ) ) ) )
87 86 adantl ⊢ ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = 𝑁 ) → ( ( lastS ‘ 𝑎 ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ↔ ( lastS ‘ 𝑎 ) = ( 𝑎 ‘ ( ( ♯ ‘ 𝑎 ) − 1 ) ) ) )
88 82 87 mpbird ⊢ ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = 𝑁 ) → ( lastS ‘ 𝑎 ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) )
89 36 88 syl ⊢ ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( lastS ‘ 𝑎 ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) )
90 89 eqcomd ⊢ ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑎 ‘ ( 𝑁 − 1 ) ) = ( lastS ‘ 𝑎 ) )
91 90 adantr ⊢ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) → ( 𝑎 ‘ ( 𝑁 − 1 ) ) = ( lastS ‘ 𝑎 ) )
92 91 ad2antrl ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑎 ‘ ( 𝑁 − 1 ) ) = ( lastS ‘ 𝑎 ) )
93 80 92 eqeq12d ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ↔ ( lastS ‘ 𝑝 ) = ( lastS ‘ 𝑎 ) ) )
94 93 biimpd ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) → ( lastS ‘ 𝑝 ) = ( lastS ‘ 𝑎 ) ) )
95 94 adantld ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) → ( lastS ‘ 𝑝 ) = ( lastS ‘ 𝑎 ) ) )
96 95 imp ⊢ ( ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ∧ ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) ) → ( lastS ‘ 𝑝 ) = ( lastS ‘ 𝑎 ) )
97 64 74 96 3jca ⊢ ( ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ∧ ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) ) → ( ( 𝑝 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) ∧ ( 𝑝 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) ∧ ( lastS ‘ 𝑝 ) = ( lastS ‘ 𝑎 ) ) )
98 97 3adant1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ∧ ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) ) → ( ( 𝑝 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) ∧ ( 𝑝 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) ∧ ( lastS ‘ 𝑝 ) = ( lastS ‘ 𝑎 ) ) )
99 1 clwwlknwrd ⊢ ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑝 ∈ Word 𝑉 )
100 99 ad3antrrr ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → 𝑝 ∈ Word 𝑉 )
101 100 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ∧ ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) ) → 𝑝 ∈ Word 𝑉 )
102 1 clwwlknwrd ⊢ ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑎 ∈ Word 𝑉 )
103 102 adantr ⊢ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) → 𝑎 ∈ Word 𝑉 )
104 103 ad2antrl ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → 𝑎 ∈ Word 𝑉 )
105 104 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ∧ ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) ) → 𝑎 ∈ Word 𝑉 )
106 clwwlknlen ⊢ ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ♯ ‘ 𝑝 ) = 𝑁 )
107 eluz2b1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) )
108 breq2 ⊢ ( 𝑁 = ( ♯ ‘ 𝑝 ) → ( 1 < 𝑁 ↔ 1 < ( ♯ ‘ 𝑝 ) ) )
109 108 eqcoms ⊢ ( ( ♯ ‘ 𝑝 ) = 𝑁 → ( 1 < 𝑁 ↔ 1 < ( ♯ ‘ 𝑝 ) ) )
110 109 biimpcd ⊢ ( 1 < 𝑁 → ( ( ♯ ‘ 𝑝 ) = 𝑁 → 1 < ( ♯ ‘ 𝑝 ) ) )
111 107 110 simplbiim ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ♯ ‘ 𝑝 ) = 𝑁 → 1 < ( ♯ ‘ 𝑝 ) ) )
112 14 106 111 syl2imc ⊢ ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 < ( ♯ ‘ 𝑝 ) ) )
113 112 ad3antrrr ⊢ ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 < ( ♯ ‘ 𝑝 ) ) )
114 113 impcom ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) → 1 < ( ♯ ‘ 𝑝 ) )
115 114 3adant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ∧ ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) ) → 1 < ( ♯ ‘ 𝑝 ) )
116 2swrd2eqwrdeq ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ 𝑎 ∈ Word 𝑉 ∧ 1 < ( ♯ ‘ 𝑝 ) ) → ( 𝑝 = 𝑎 ↔ ( ( ♯ ‘ 𝑝 ) = ( ♯ ‘ 𝑎 ) ∧ ( ( 𝑝 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) ∧ ( 𝑝 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) ∧ ( lastS ‘ 𝑝 ) = ( lastS ‘ 𝑎 ) ) ) ) )
117 101 105 115 116 syl3anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ∧ ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) ) → ( 𝑝 = 𝑎 ↔ ( ( ♯ ‘ 𝑝 ) = ( ♯ ‘ 𝑎 ) ∧ ( ( 𝑝 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 prefix ( ( ♯ ‘ 𝑝 ) − 2 ) ) ∧ ( 𝑝 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) = ( 𝑎 ‘ ( ( ♯ ‘ 𝑝 ) − 2 ) ) ∧ ( lastS ‘ 𝑝 ) = ( lastS ‘ 𝑎 ) ) ) ) )
118 53 98 117 mpbir2and ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ∧ ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) ) → 𝑝 = 𝑎 )
119 118 3exp ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) → 𝑝 = 𝑎 ) ) )
120 119 3ad2ant3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑝 ‘ 0 ) = 𝑋 ) ∧ ( 𝑝 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ∧ ( ( 𝑎 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ∧ ( 𝑎 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) → 𝑝 = 𝑎 ) ) )
121 25 120 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ∧ 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ) → ( ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) → 𝑝 = 𝑎 ) ) )
122 121 imp ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ∧ 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ) ) → ( ( ( 𝑝 prefix ( 𝑁 − 2 ) ) = ( 𝑎 prefix ( 𝑁 − 2 ) ) ∧ ( 𝑝 ‘ ( 𝑁 − 1 ) ) = ( 𝑎 ‘ ( 𝑁 − 1 ) ) ) → 𝑝 = 𝑎 ) )
123 13 122 biimtrid ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ∧ 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ) ) → ( ⟨ ( 𝑝 prefix ( 𝑁 − 2 ) ) , ( 𝑝 ‘ ( 𝑁 − 1 ) ) ⟩ = ⟨ ( 𝑎 prefix ( 𝑁 − 2 ) ) , ( 𝑎 ‘ ( 𝑁 − 1 ) ) ⟩ → 𝑝 = 𝑎 ) )
124 10 123 sylbid ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ∧ 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ) ) → ( ( 𝑇 ‘ 𝑝 ) = ( 𝑇 ‘ 𝑎 ) → 𝑝 = 𝑎 ) )
125 124 ralrimivva ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ∀ 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ∀ 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ( ( 𝑇 ‘ 𝑝 ) = ( 𝑇 ‘ 𝑎 ) → 𝑝 = 𝑎 ) )
126 dff13 ⊢ ( 𝑇 : ( 𝑋 𝐶 𝑁 ) –1-1→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ↔ ( 𝑇 : ( 𝑋 𝐶 𝑁 ) ⟶ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ∧ ∀ 𝑝 ∈ ( 𝑋 𝐶 𝑁 ) ∀ 𝑎 ∈ ( 𝑋 𝐶 𝑁 ) ( ( 𝑇 ‘ 𝑝 ) = ( 𝑇 ‘ 𝑎 ) → 𝑝 = 𝑎 ) ) )
127 5 125 126 sylanbrc ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑇 : ( 𝑋 𝐶 𝑁 ) –1-1→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )