Metamath Proof Explorer

Theorem clwwlkf1

Description: Lemma 3 for clwwlkf1o : F is a 1-1 function. (Contributed by AV, 28-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses clwwlkf1o.d 
|- D = { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) }
clwwlkf1o.f 
|- F = ( t e. D |-> ( t prefix N ) )
Assertion clwwlkf1 
|- ( N e. NN -> F : D -1-1-> ( N ClWWalksN G ) )

Proof

Step Hyp Ref Expression
1 clwwlkf1o.d 
 |-  D = { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) }
2 clwwlkf1o.f 
 |-  F = ( t e. D |-> ( t prefix N ) )
3 1 2 clwwlkf 
 |-  ( N e. NN -> F : D --> ( N ClWWalksN G ) )
4 1 2 clwwlkfv 
 |-  ( x e. D -> ( F ` x ) = ( x prefix N ) )
5 1 2 clwwlkfv 
 |-  ( y e. D -> ( F ` y ) = ( y prefix N ) )
6 4 5 eqeqan12d 
 |-  ( ( x e. D /\ y e. D ) -> ( ( F ` x ) = ( F ` y ) <-> ( x prefix N ) = ( y prefix N ) ) )
7 6 adantl 
 |-  ( ( N e. NN /\ ( x e. D /\ y e. D ) ) -> ( ( F ` x ) = ( F ` y ) <-> ( x prefix N ) = ( y prefix N ) ) )
8 fveq2 
 |-  ( w = x -> ( lastS ` w ) = ( lastS ` x ) )
9 fveq1 
 |-  ( w = x -> ( w ` 0 ) = ( x ` 0 ) )
10 8 9 eqeq12d 
 |-  ( w = x -> ( ( lastS ` w ) = ( w ` 0 ) <-> ( lastS ` x ) = ( x ` 0 ) ) )
11 10 1 elrab2 
 |-  ( x e. D <-> ( x e. ( N WWalksN G ) /\ ( lastS ` x ) = ( x ` 0 ) ) )
12 fveq2 
 |-  ( w = y -> ( lastS ` w ) = ( lastS ` y ) )
13 fveq1 
 |-  ( w = y -> ( w ` 0 ) = ( y ` 0 ) )
14 12 13 eqeq12d 
 |-  ( w = y -> ( ( lastS ` w ) = ( w ` 0 ) <-> ( lastS ` y ) = ( y ` 0 ) ) )
15 14 1 elrab2 
 |-  ( y e. D <-> ( y e. ( N WWalksN G ) /\ ( lastS ` y ) = ( y ` 0 ) ) )
16 11 15 anbi12i 
 |-  ( ( x e. D /\ y e. D ) <-> ( ( x e. ( N WWalksN G ) /\ ( lastS ` x ) = ( x ` 0 ) ) /\ ( y e. ( N WWalksN G ) /\ ( lastS ` y ) = ( y ` 0 ) ) ) )
17 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
18 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
19 17 18 wwlknp 
 |-  ( x e. ( N WWalksN G ) -> ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( x ` i ) , ( x ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
20 17 18 wwlknp 
 |-  ( y e. ( N WWalksN G ) -> ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
21 simprlr 
 |-  ( ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) -> ( # ` x ) = ( N + 1 ) )
22 simpllr 
 |-  ( ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) -> ( # ` y ) = ( N + 1 ) )
23 21 22 eqtr4d 
 |-  ( ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) -> ( # ` x ) = ( # ` y ) )
24 23 ad2antlr 
 |-  ( ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) /\ ( x prefix N ) = ( y prefix N ) ) -> ( # ` x ) = ( # ` y ) )
25 nncn 
 |-  ( N e. NN -> N e. CC )
26 ax-1cn 
 |-  1 e. CC
27 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
28 27 eqcomd 
 |-  ( ( N e. CC /\ 1 e. CC ) -> N = ( ( N + 1 ) - 1 ) )
29 25 26 28 sylancl 
 |-  ( N e. NN -> N = ( ( N + 1 ) - 1 ) )
30 oveq1 
 |-  ( ( # ` x ) = ( N + 1 ) -> ( ( # ` x ) - 1 ) = ( ( N + 1 ) - 1 ) )
31 30 eqcomd 
 |-  ( ( # ` x ) = ( N + 1 ) -> ( ( N + 1 ) - 1 ) = ( ( # ` x ) - 1 ) )
32 29 31 sylan9eqr 
 |-  ( ( ( # ` x ) = ( N + 1 ) /\ N e. NN ) -> N = ( ( # ` x ) - 1 ) )
33 32 oveq2d 
 |-  ( ( ( # ` x ) = ( N + 1 ) /\ N e. NN ) -> ( x prefix N ) = ( x prefix ( ( # ` x ) - 1 ) ) )
34 32 oveq2d 
 |-  ( ( ( # ` x ) = ( N + 1 ) /\ N e. NN ) -> ( y prefix N ) = ( y prefix ( ( # ` x ) - 1 ) ) )
35 33 34 eqeq12d 
 |-  ( ( ( # ` x ) = ( N + 1 ) /\ N e. NN ) -> ( ( x prefix N ) = ( y prefix N ) <-> ( x prefix ( ( # ` x ) - 1 ) ) = ( y prefix ( ( # ` x ) - 1 ) ) ) )
36 35 ex 
 |-  ( ( # ` x ) = ( N + 1 ) -> ( N e. NN -> ( ( x prefix N ) = ( y prefix N ) <-> ( x prefix ( ( # ` x ) - 1 ) ) = ( y prefix ( ( # ` x ) - 1 ) ) ) ) )
37 36 ad2antlr 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) -> ( N e. NN -> ( ( x prefix N ) = ( y prefix N ) <-> ( x prefix ( ( # ` x ) - 1 ) ) = ( y prefix ( ( # ` x ) - 1 ) ) ) ) )
38 37 adantl 
 |-  ( ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) -> ( N e. NN -> ( ( x prefix N ) = ( y prefix N ) <-> ( x prefix ( ( # ` x ) - 1 ) ) = ( y prefix ( ( # ` x ) - 1 ) ) ) ) )
39 38 impcom 
 |-  ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) -> ( ( x prefix N ) = ( y prefix N ) <-> ( x prefix ( ( # ` x ) - 1 ) ) = ( y prefix ( ( # ` x ) - 1 ) ) ) )
40 39 biimpa 
 |-  ( ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) /\ ( x prefix N ) = ( y prefix N ) ) -> ( x prefix ( ( # ` x ) - 1 ) ) = ( y prefix ( ( # ` x ) - 1 ) ) )
41 simpll 
 |-  ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) -> y e. Word ( Vtx ` G ) )
42 simpll 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) -> x e. Word ( Vtx ` G ) )
43 41 42 anim12ci 
 |-  ( ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) -> ( x e. Word ( Vtx ` G ) /\ y e. Word ( Vtx ` G ) ) )
44 43 adantl 
 |-  ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) -> ( x e. Word ( Vtx ` G ) /\ y e. Word ( Vtx ` G ) ) )
45 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
46 0nn0 
 |-  0 e. NN0
47 45 46 jctil 
 |-  ( N e. NN -> ( 0 e. NN0 /\ N e. NN0 ) )
48 47 adantr 
 |-  ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) -> ( 0 e. NN0 /\ N e. NN0 ) )
49 nnre 
 |-  ( N e. NN -> N e. RR )
50 49 lep1d 
 |-  ( N e. NN -> N <_ ( N + 1 ) )
51 breq2 
 |-  ( ( # ` x ) = ( N + 1 ) -> ( N <_ ( # ` x ) <-> N <_ ( N + 1 ) ) )
52 50 51 syl5ibr 
 |-  ( ( # ` x ) = ( N + 1 ) -> ( N e. NN -> N <_ ( # ` x ) ) )
53 52 ad2antlr 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) -> ( N e. NN -> N <_ ( # ` x ) ) )
54 53 adantl 
 |-  ( ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) -> ( N e. NN -> N <_ ( # ` x ) ) )
55 54 impcom 
 |-  ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) -> N <_ ( # ` x ) )
56 breq2 
 |-  ( ( # ` y ) = ( N + 1 ) -> ( N <_ ( # ` y ) <-> N <_ ( N + 1 ) ) )
57 50 56 syl5ibr 
 |-  ( ( # ` y ) = ( N + 1 ) -> ( N e. NN -> N <_ ( # ` y ) ) )
58 57 ad2antlr 
 |-  ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) -> ( N e. NN -> N <_ ( # ` y ) ) )
59 58 adantr 
 |-  ( ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) -> ( N e. NN -> N <_ ( # ` y ) ) )
60 59 impcom 
 |-  ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) -> N <_ ( # ` y ) )
61 pfxval 
 |-  ( ( x e. Word ( Vtx ` G ) /\ N e. NN0 ) -> ( x prefix N ) = ( x substr <. 0 , N >. ) )
62 61 ad2ant2rl 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ y e. Word ( Vtx ` G ) ) /\ ( 0 e. NN0 /\ N e. NN0 ) ) -> ( x prefix N ) = ( x substr <. 0 , N >. ) )
63 pfxval 
 |-  ( ( y e. Word ( Vtx ` G ) /\ N e. NN0 ) -> ( y prefix N ) = ( y substr <. 0 , N >. ) )
64 63 ad2ant2l 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ y e. Word ( Vtx ` G ) ) /\ ( 0 e. NN0 /\ N e. NN0 ) ) -> ( y prefix N ) = ( y substr <. 0 , N >. ) )
65 62 64 eqeq12d 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ y e. Word ( Vtx ` G ) ) /\ ( 0 e. NN0 /\ N e. NN0 ) ) -> ( ( x prefix N ) = ( y prefix N ) <-> ( x substr <. 0 , N >. ) = ( y substr <. 0 , N >. ) ) )
66 65 3adant3 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ y e. Word ( Vtx ` G ) ) /\ ( 0 e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` x ) /\ N <_ ( # ` y ) ) ) -> ( ( x prefix N ) = ( y prefix N ) <-> ( x substr <. 0 , N >. ) = ( y substr <. 0 , N >. ) ) )
67 swrdspsleq 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ y e. Word ( Vtx ` G ) ) /\ ( 0 e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` x ) /\ N <_ ( # ` y ) ) ) -> ( ( x substr <. 0 , N >. ) = ( y substr <. 0 , N >. ) <-> A. i e. ( 0 ..^ N ) ( x ` i ) = ( y ` i ) ) )
68 66 67 bitrd 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ y e. Word ( Vtx ` G ) ) /\ ( 0 e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` x ) /\ N <_ ( # ` y ) ) ) -> ( ( x prefix N ) = ( y prefix N ) <-> A. i e. ( 0 ..^ N ) ( x ` i ) = ( y ` i ) ) )
69 44 48 55 60 68 syl112anc 
 |-  ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) -> ( ( x prefix N ) = ( y prefix N ) <-> A. i e. ( 0 ..^ N ) ( x ` i ) = ( y ` i ) ) )
70 lbfzo0 
 |-  ( 0 e. ( 0 ..^ N ) <-> N e. NN )
71 70 biimpri 
 |-  ( N e. NN -> 0 e. ( 0 ..^ N ) )
72 71 adantr 
 |-  ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) -> 0 e. ( 0 ..^ N ) )
73 fveq2 
 |-  ( i = 0 -> ( x ` i ) = ( x ` 0 ) )
74 fveq2 
 |-  ( i = 0 -> ( y ` i ) = ( y ` 0 ) )
75 73 74 eqeq12d 
 |-  ( i = 0 -> ( ( x ` i ) = ( y ` i ) <-> ( x ` 0 ) = ( y ` 0 ) ) )
76 75 rspcv 
 |-  ( 0 e. ( 0 ..^ N ) -> ( A. i e. ( 0 ..^ N ) ( x ` i ) = ( y ` i ) -> ( x ` 0 ) = ( y ` 0 ) ) )
77 72 76 syl 
 |-  ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) -> ( A. i e. ( 0 ..^ N ) ( x ` i ) = ( y ` i ) -> ( x ` 0 ) = ( y ` 0 ) ) )
78 69 77 sylbid 
 |-  ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) -> ( ( x prefix N ) = ( y prefix N ) -> ( x ` 0 ) = ( y ` 0 ) ) )
79 78 imp 
 |-  ( ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) /\ ( x prefix N ) = ( y prefix N ) ) -> ( x ` 0 ) = ( y ` 0 ) )
80 simpr 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) -> ( lastS ` x ) = ( x ` 0 ) )
81 simpr 
 |-  ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) -> ( lastS ` y ) = ( y ` 0 ) )
82 80 81 eqeqan12rd 
 |-  ( ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) -> ( ( lastS ` x ) = ( lastS ` y ) <-> ( x ` 0 ) = ( y ` 0 ) ) )
83 82 ad2antlr 
 |-  ( ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) /\ ( x prefix N ) = ( y prefix N ) ) -> ( ( lastS ` x ) = ( lastS ` y ) <-> ( x ` 0 ) = ( y ` 0 ) ) )
84 79 83 mpbird 
 |-  ( ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) /\ ( x prefix N ) = ( y prefix N ) ) -> ( lastS ` x ) = ( lastS ` y ) )
85 24 40 84 jca32 
 |-  ( ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) /\ ( x prefix N ) = ( y prefix N ) ) -> ( ( # ` x ) = ( # ` y ) /\ ( ( x prefix ( ( # ` x ) - 1 ) ) = ( y prefix ( ( # ` x ) - 1 ) ) /\ ( lastS ` x ) = ( lastS ` y ) ) ) )
86 42 adantl 
 |-  ( ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) -> x e. Word ( Vtx ` G ) )
87 86 adantl 
 |-  ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) -> x e. Word ( Vtx ` G ) )
88 41 adantr 
 |-  ( ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) -> y e. Word ( Vtx ` G ) )
89 88 adantl 
 |-  ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) -> y e. Word ( Vtx ` G ) )
90 1red 
 |-  ( N e. NN -> 1 e. RR )
91 nngt0 
 |-  ( N e. NN -> 0 < N )
92 0lt1 
 |-  0 < 1
93 92 a1i 
 |-  ( N e. NN -> 0 < 1 )
94 49 90 91 93 addgt0d 
 |-  ( N e. NN -> 0 < ( N + 1 ) )
95 breq2 
 |-  ( ( # ` x ) = ( N + 1 ) -> ( 0 < ( # ` x ) <-> 0 < ( N + 1 ) ) )
96 94 95 syl5ibr 
 |-  ( ( # ` x ) = ( N + 1 ) -> ( N e. NN -> 0 < ( # ` x ) ) )
97 96 ad2antlr 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) -> ( N e. NN -> 0 < ( # ` x ) ) )
98 97 adantl 
 |-  ( ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) -> ( N e. NN -> 0 < ( # ` x ) ) )
99 98 impcom 
 |-  ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) -> 0 < ( # ` x ) )
100 87 89 99 3jca 
 |-  ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) -> ( x e. Word ( Vtx ` G ) /\ y e. Word ( Vtx ` G ) /\ 0 < ( # ` x ) ) )
101 100 adantr 
 |-  ( ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) /\ ( x prefix N ) = ( y prefix N ) ) -> ( x e. Word ( Vtx ` G ) /\ y e. Word ( Vtx ` G ) /\ 0 < ( # ` x ) ) )
102 pfxsuff1eqwrdeq 
 |-  ( ( x e. Word ( Vtx ` G ) /\ y e. Word ( Vtx ` G ) /\ 0 < ( # ` x ) ) -> ( x = y <-> ( ( # ` x ) = ( # ` y ) /\ ( ( x prefix ( ( # ` x ) - 1 ) ) = ( y prefix ( ( # ` x ) - 1 ) ) /\ ( lastS ` x ) = ( lastS ` y ) ) ) ) )
103 101 102 syl 
 |-  ( ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) /\ ( x prefix N ) = ( y prefix N ) ) -> ( x = y <-> ( ( # ` x ) = ( # ` y ) /\ ( ( x prefix ( ( # ` x ) - 1 ) ) = ( y prefix ( ( # ` x ) - 1 ) ) /\ ( lastS ` x ) = ( lastS ` y ) ) ) ) )
104 85 103 mpbird 
 |-  ( ( ( N e. NN /\ ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) ) /\ ( x prefix N ) = ( y prefix N ) ) -> x = y )
105 104 exp31 
 |-  ( N e. NN -> ( ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) /\ ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) ) -> ( ( x prefix N ) = ( y prefix N ) -> x = y ) ) )
106 105 expdcom 
 |-  ( ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) /\ ( lastS ` y ) = ( y ` 0 ) ) -> ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) -> ( N e. NN -> ( ( x prefix N ) = ( y prefix N ) -> x = y ) ) ) )
107 106 ex 
 |-  ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) ) -> ( ( lastS ` y ) = ( y ` 0 ) -> ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) -> ( N e. NN -> ( ( x prefix N ) = ( y prefix N ) -> x = y ) ) ) ) )
108 107 3adant3 
 |-  ( ( y e. Word ( Vtx ` G ) /\ ( # ` y ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( lastS ` y ) = ( y ` 0 ) -> ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) -> ( N e. NN -> ( ( x prefix N ) = ( y prefix N ) -> x = y ) ) ) ) )
109 20 108 syl 
 |-  ( y e. ( N WWalksN G ) -> ( ( lastS ` y ) = ( y ` 0 ) -> ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) -> ( N e. NN -> ( ( x prefix N ) = ( y prefix N ) -> x = y ) ) ) ) )
110 109 imp 
 |-  ( ( y e. ( N WWalksN G ) /\ ( lastS ` y ) = ( y ` 0 ) ) -> ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) /\ ( lastS ` x ) = ( x ` 0 ) ) -> ( N e. NN -> ( ( x prefix N ) = ( y prefix N ) -> x = y ) ) ) )
111 110 expdcom 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) ) -> ( ( lastS ` x ) = ( x ` 0 ) -> ( ( y e. ( N WWalksN G ) /\ ( lastS ` y ) = ( y ` 0 ) ) -> ( N e. NN -> ( ( x prefix N ) = ( y prefix N ) -> x = y ) ) ) ) )
112 111 3adant3 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( x ` i ) , ( x ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( lastS ` x ) = ( x ` 0 ) -> ( ( y e. ( N WWalksN G ) /\ ( lastS ` y ) = ( y ` 0 ) ) -> ( N e. NN -> ( ( x prefix N ) = ( y prefix N ) -> x = y ) ) ) ) )
113 19 112 syl 
 |-  ( x e. ( N WWalksN G ) -> ( ( lastS ` x ) = ( x ` 0 ) -> ( ( y e. ( N WWalksN G ) /\ ( lastS ` y ) = ( y ` 0 ) ) -> ( N e. NN -> ( ( x prefix N ) = ( y prefix N ) -> x = y ) ) ) ) )
114 113 imp31 
 |-  ( ( ( x e. ( N WWalksN G ) /\ ( lastS ` x ) = ( x ` 0 ) ) /\ ( y e. ( N WWalksN G ) /\ ( lastS ` y ) = ( y ` 0 ) ) ) -> ( N e. NN -> ( ( x prefix N ) = ( y prefix N ) -> x = y ) ) )
115 114 com12 
 |-  ( N e. NN -> ( ( ( x e. ( N WWalksN G ) /\ ( lastS ` x ) = ( x ` 0 ) ) /\ ( y e. ( N WWalksN G ) /\ ( lastS ` y ) = ( y ` 0 ) ) ) -> ( ( x prefix N ) = ( y prefix N ) -> x = y ) ) )
116 16 115 syl5bi 
 |-  ( N e. NN -> ( ( x e. D /\ y e. D ) -> ( ( x prefix N ) = ( y prefix N ) -> x = y ) ) )
117 116 imp 
 |-  ( ( N e. NN /\ ( x e. D /\ y e. D ) ) -> ( ( x prefix N ) = ( y prefix N ) -> x = y ) )
118 7 117 sylbid 
 |-  ( ( N e. NN /\ ( x e. D /\ y e. D ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
119 118 ralrimivva 
 |-  ( N e. NN -> A. x e. D A. y e. D ( ( F ` x ) = ( F ` y ) -> x = y ) )
120 dff13 
 |-  ( F : D -1-1-> ( N ClWWalksN G ) <-> ( F : D --> ( N ClWWalksN G ) /\ A. x e. D A. y e. D ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
121 3 119 120 sylanbrc 
 |-  ( N e. NN -> F : D -1-1-> ( N ClWWalksN G ) )