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 ) )