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 
|- V = ( Vtx ` G )
extwwlkfab.c 
|- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
extwwlkfab.f 
|- F = ( X ( ClWWalksNOn ` G ) ( N - 2 ) )
numclwwlk.t 
|- T = ( u e. ( X C N ) |-> <. ( u prefix ( N - 2 ) ) , ( u ` ( N - 1 ) ) >. )
Assertion numclwwlk1lem2f1 
|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> T : ( X C N ) -1-1-> ( F X. ( G NeighbVtx X ) ) )

Proof

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