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