Step |
Hyp |
Ref |
Expression |
1 |
|
clwwlkext2edg.v |
|- V = ( Vtx ` G ) |
2 |
|
clwwlkext2edg.e |
|- E = ( Edg ` G ) |
3 |
|
wwlknbp1 |
|- ( W e. ( N WWalksN G ) -> ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) |
4 |
1
|
wrdeqi |
|- Word V = Word ( Vtx ` G ) |
5 |
4
|
eleq2i |
|- ( W e. Word V <-> W e. Word ( Vtx ` G ) ) |
6 |
5
|
biimpri |
|- ( W e. Word ( Vtx ` G ) -> W e. Word V ) |
7 |
6
|
3ad2ant2 |
|- ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> W e. Word V ) |
8 |
7
|
ad2antlr |
|- ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> W e. Word V ) |
9 |
|
s1cl |
|- ( Z e. V -> <" Z "> e. Word V ) |
10 |
9
|
adantl |
|- ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> <" Z "> e. Word V ) |
11 |
|
ccatcl |
|- ( ( W e. Word V /\ <" Z "> e. Word V ) -> ( W ++ <" Z "> ) e. Word V ) |
12 |
8 10 11
|
syl2anc |
|- ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> ( W ++ <" Z "> ) e. Word V ) |
13 |
12
|
adantr |
|- ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> ( W ++ <" Z "> ) e. Word V ) |
14 |
1 2
|
wwlknp |
|- ( W e. ( N WWalksN G ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) |
15 |
|
simplll |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> W e. Word V ) |
16 |
9
|
adantr |
|- ( ( Z e. V /\ N e. NN0 ) -> <" Z "> e. Word V ) |
17 |
16
|
ad2antlr |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> <" Z "> e. Word V ) |
18 |
|
elfzo0 |
|- ( i e. ( 0 ..^ N ) <-> ( i e. NN0 /\ N e. NN /\ i < N ) ) |
19 |
|
simp1 |
|- ( ( i e. NN0 /\ N e. NN /\ i < N ) -> i e. NN0 ) |
20 |
|
peano2nn |
|- ( N e. NN -> ( N + 1 ) e. NN ) |
21 |
20
|
3ad2ant2 |
|- ( ( i e. NN0 /\ N e. NN /\ i < N ) -> ( N + 1 ) e. NN ) |
22 |
|
nn0re |
|- ( i e. NN0 -> i e. RR ) |
23 |
22
|
3ad2ant1 |
|- ( ( i e. NN0 /\ N e. NN /\ i < N ) -> i e. RR ) |
24 |
|
nnre |
|- ( N e. NN -> N e. RR ) |
25 |
24
|
3ad2ant2 |
|- ( ( i e. NN0 /\ N e. NN /\ i < N ) -> N e. RR ) |
26 |
|
peano2re |
|- ( N e. RR -> ( N + 1 ) e. RR ) |
27 |
24 26
|
syl |
|- ( N e. NN -> ( N + 1 ) e. RR ) |
28 |
27
|
3ad2ant2 |
|- ( ( i e. NN0 /\ N e. NN /\ i < N ) -> ( N + 1 ) e. RR ) |
29 |
|
simp3 |
|- ( ( i e. NN0 /\ N e. NN /\ i < N ) -> i < N ) |
30 |
24
|
ltp1d |
|- ( N e. NN -> N < ( N + 1 ) ) |
31 |
30
|
3ad2ant2 |
|- ( ( i e. NN0 /\ N e. NN /\ i < N ) -> N < ( N + 1 ) ) |
32 |
23 25 28 29 31
|
lttrd |
|- ( ( i e. NN0 /\ N e. NN /\ i < N ) -> i < ( N + 1 ) ) |
33 |
|
elfzo0 |
|- ( i e. ( 0 ..^ ( N + 1 ) ) <-> ( i e. NN0 /\ ( N + 1 ) e. NN /\ i < ( N + 1 ) ) ) |
34 |
19 21 32 33
|
syl3anbrc |
|- ( ( i e. NN0 /\ N e. NN /\ i < N ) -> i e. ( 0 ..^ ( N + 1 ) ) ) |
35 |
18 34
|
sylbi |
|- ( i e. ( 0 ..^ N ) -> i e. ( 0 ..^ ( N + 1 ) ) ) |
36 |
35
|
adantl |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> i e. ( 0 ..^ ( N + 1 ) ) ) |
37 |
|
oveq2 |
|- ( ( # ` W ) = ( N + 1 ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ ( N + 1 ) ) ) |
38 |
37
|
adantl |
|- ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ ( N + 1 ) ) ) |
39 |
38
|
eleq2d |
|- ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ ( # ` W ) ) <-> i e. ( 0 ..^ ( N + 1 ) ) ) ) |
40 |
39
|
ad2antrr |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( i e. ( 0 ..^ ( # ` W ) ) <-> i e. ( 0 ..^ ( N + 1 ) ) ) ) |
41 |
36 40
|
mpbird |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> i e. ( 0 ..^ ( # ` W ) ) ) |
42 |
|
ccatval1 |
|- ( ( W e. Word V /\ <" Z "> e. Word V /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" Z "> ) ` i ) = ( W ` i ) ) |
43 |
15 17 41 42
|
syl3anc |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( W ++ <" Z "> ) ` i ) = ( W ` i ) ) |
44 |
|
fzonn0p1p1 |
|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) ) |
45 |
44
|
adantl |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) ) |
46 |
37
|
eleq2d |
|- ( ( # ` W ) = ( N + 1 ) -> ( ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) <-> ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) ) ) |
47 |
46
|
ad3antlr |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) <-> ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) ) ) |
48 |
45 47
|
mpbird |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) ) |
49 |
|
ccatval1 |
|- ( ( W e. Word V /\ <" Z "> e. Word V /\ ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" Z "> ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) ) |
50 |
15 17 48 49
|
syl3anc |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( W ++ <" Z "> ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) ) |
51 |
43 50
|
preq12d |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) /\ i e. ( 0 ..^ N ) ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) |
52 |
51
|
ex |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( i e. ( 0 ..^ N ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) ) |
53 |
52
|
expcom |
|- ( ( Z e. V /\ N e. NN0 ) -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ N ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) ) ) |
54 |
53
|
expcom |
|- ( N e. NN0 -> ( Z e. V -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ N ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) ) ) ) |
55 |
54
|
3ad2ant1 |
|- ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( Z e. V -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ N ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) ) ) ) |
56 |
55
|
imp |
|- ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ N ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) ) ) |
57 |
56
|
expdcom |
|- ( W e. Word V -> ( ( # ` W ) = ( N + 1 ) -> ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> ( i e. ( 0 ..^ N ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) ) ) ) |
58 |
57
|
3imp1 |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ i e. ( 0 ..^ N ) ) -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } ) |
59 |
58
|
eleq1d |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ i e. ( 0 ..^ N ) ) -> ( { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) |
60 |
59
|
ralbidva |
|- ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> ( A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) |
61 |
60
|
biimprd |
|- ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> ( A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E -> A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) ) |
62 |
61
|
3exp |
|- ( W e. Word V -> ( ( # ` W ) = ( N + 1 ) -> ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> ( A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E -> A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) ) ) ) |
63 |
62
|
com34 |
|- ( W e. Word V -> ( ( # ` W ) = ( N + 1 ) -> ( A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E -> ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) ) ) ) |
64 |
63
|
3imp1 |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) |
65 |
64
|
adantr |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) |
66 |
|
simpll |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> W e. Word V ) |
67 |
9
|
ad2antrl |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> <" Z "> e. Word V ) |
68 |
|
nn0p1gt0 |
|- ( N e. NN0 -> 0 < ( N + 1 ) ) |
69 |
68
|
ad2antll |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> 0 < ( N + 1 ) ) |
70 |
|
breq2 |
|- ( ( # ` W ) = ( N + 1 ) -> ( 0 < ( # ` W ) <-> 0 < ( N + 1 ) ) ) |
71 |
70
|
ad2antlr |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( 0 < ( # ` W ) <-> 0 < ( N + 1 ) ) ) |
72 |
69 71
|
mpbird |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> 0 < ( # ` W ) ) |
73 |
|
hashneq0 |
|- ( W e. Word V -> ( 0 < ( # ` W ) <-> W =/= (/) ) ) |
74 |
73
|
ad2antrr |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( 0 < ( # ` W ) <-> W =/= (/) ) ) |
75 |
72 74
|
mpbid |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> W =/= (/) ) |
76 |
|
ccatval1lsw |
|- ( ( W e. Word V /\ <" Z "> e. Word V /\ W =/= (/) ) -> ( ( W ++ <" Z "> ) ` ( ( # ` W ) - 1 ) ) = ( lastS ` W ) ) |
77 |
66 67 75 76
|
syl3anc |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( W ++ <" Z "> ) ` ( ( # ` W ) - 1 ) ) = ( lastS ` W ) ) |
78 |
|
oveq1 |
|- ( ( # ` W ) = ( N + 1 ) -> ( ( # ` W ) - 1 ) = ( ( N + 1 ) - 1 ) ) |
79 |
78
|
ad2antlr |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( # ` W ) - 1 ) = ( ( N + 1 ) - 1 ) ) |
80 |
|
nn0cn |
|- ( N e. NN0 -> N e. CC ) |
81 |
80
|
ad2antll |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> N e. CC ) |
82 |
|
pncan1 |
|- ( N e. CC -> ( ( N + 1 ) - 1 ) = N ) |
83 |
81 82
|
syl |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( N + 1 ) - 1 ) = N ) |
84 |
79 83
|
eqtrd |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( # ` W ) - 1 ) = N ) |
85 |
84
|
fveq2d |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( W ++ <" Z "> ) ` ( ( # ` W ) - 1 ) ) = ( ( W ++ <" Z "> ) ` N ) ) |
86 |
77 85
|
eqtr3d |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( lastS ` W ) = ( ( W ++ <" Z "> ) ` N ) ) |
87 |
|
ccatws1ls |
|- ( ( W e. Word V /\ Z e. V ) -> ( ( W ++ <" Z "> ) ` ( # ` W ) ) = Z ) |
88 |
87
|
ad2ant2r |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( W ++ <" Z "> ) ` ( # ` W ) ) = Z ) |
89 |
|
fveq2 |
|- ( ( # ` W ) = ( N + 1 ) -> ( ( W ++ <" Z "> ) ` ( # ` W ) ) = ( ( W ++ <" Z "> ) ` ( N + 1 ) ) ) |
90 |
89
|
ad2antlr |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> ( ( W ++ <" Z "> ) ` ( # ` W ) ) = ( ( W ++ <" Z "> ) ` ( N + 1 ) ) ) |
91 |
88 90
|
eqtr3d |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> Z = ( ( W ++ <" Z "> ) ` ( N + 1 ) ) ) |
92 |
86 91
|
preq12d |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ ( Z e. V /\ N e. NN0 ) ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) |
93 |
92
|
expcom |
|- ( ( Z e. V /\ N e. NN0 ) -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) ) |
94 |
93
|
expcom |
|- ( N e. NN0 -> ( Z e. V -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) ) ) |
95 |
94
|
3ad2ant1 |
|- ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( Z e. V -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) ) ) |
96 |
95
|
imp |
|- ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) ) |
97 |
96
|
com12 |
|- ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) ) |
98 |
97
|
3adant3 |
|- ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) ) |
99 |
98
|
imp |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> { ( lastS ` W ) , Z } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) |
100 |
99
|
eleq1d |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> ( { ( lastS ` W ) , Z } e. E <-> { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } e. E ) ) |
101 |
100
|
biimpa |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } e. E ) |
102 |
|
simprl1 |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> N e. NN0 ) |
103 |
102
|
adantr |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> N e. NN0 ) |
104 |
|
fveq2 |
|- ( i = N -> ( ( W ++ <" Z "> ) ` i ) = ( ( W ++ <" Z "> ) ` N ) ) |
105 |
|
fvoveq1 |
|- ( i = N -> ( ( W ++ <" Z "> ) ` ( i + 1 ) ) = ( ( W ++ <" Z "> ) ` ( N + 1 ) ) ) |
106 |
104 105
|
preq12d |
|- ( i = N -> { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } = { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } ) |
107 |
106
|
eleq1d |
|- ( i = N -> ( { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } e. E ) ) |
108 |
107
|
ralsng |
|- ( N e. NN0 -> ( A. i e. { N } { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } e. E ) ) |
109 |
103 108
|
syl |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( A. i e. { N } { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> { ( ( W ++ <" Z "> ) ` N ) , ( ( W ++ <" Z "> ) ` ( N + 1 ) ) } e. E ) ) |
110 |
101 109
|
mpbird |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> A. i e. { N } { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) |
111 |
|
ralunb |
|- ( A. i e. ( ( 0 ..^ N ) u. { N } ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> ( A. i e. ( 0 ..^ N ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ A. i e. { N } { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) ) |
112 |
65 110 111
|
sylanbrc |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> A. i e. ( ( 0 ..^ N ) u. { N } ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) |
113 |
|
elnn0uz |
|- ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) ) |
114 |
102 113
|
sylib |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> N e. ( ZZ>= ` 0 ) ) |
115 |
114
|
adantr |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> N e. ( ZZ>= ` 0 ) ) |
116 |
|
fzosplitsn |
|- ( N e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. { N } ) ) |
117 |
115 116
|
syl |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. { N } ) ) |
118 |
117
|
raleqdv |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( A. i e. ( 0 ..^ ( N + 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> A. i e. ( ( 0 ..^ N ) u. { N } ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) ) |
119 |
112 118
|
mpbird |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> A. i e. ( 0 ..^ ( N + 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) |
120 |
|
ccatws1len |
|- ( W e. Word V -> ( # ` ( W ++ <" Z "> ) ) = ( ( # ` W ) + 1 ) ) |
121 |
120
|
3ad2ant1 |
|- ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( # ` ( W ++ <" Z "> ) ) = ( ( # ` W ) + 1 ) ) |
122 |
121
|
ad2antrr |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( # ` ( W ++ <" Z "> ) ) = ( ( # ` W ) + 1 ) ) |
123 |
122
|
oveq1d |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( ( # ` ( W ++ <" Z "> ) ) - 1 ) = ( ( ( # ` W ) + 1 ) - 1 ) ) |
124 |
|
oveq1 |
|- ( ( # ` W ) = ( N + 1 ) -> ( ( # ` W ) + 1 ) = ( ( N + 1 ) + 1 ) ) |
125 |
124
|
oveq1d |
|- ( ( # ` W ) = ( N + 1 ) -> ( ( ( # ` W ) + 1 ) - 1 ) = ( ( ( N + 1 ) + 1 ) - 1 ) ) |
126 |
|
1cnd |
|- ( N e. NN0 -> 1 e. CC ) |
127 |
80 126
|
addcld |
|- ( N e. NN0 -> ( N + 1 ) e. CC ) |
128 |
127 126
|
pncand |
|- ( N e. NN0 -> ( ( ( N + 1 ) + 1 ) - 1 ) = ( N + 1 ) ) |
129 |
128
|
3ad2ant1 |
|- ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( ( N + 1 ) + 1 ) - 1 ) = ( N + 1 ) ) |
130 |
129
|
adantr |
|- ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) -> ( ( ( N + 1 ) + 1 ) - 1 ) = ( N + 1 ) ) |
131 |
125 130
|
sylan9eq |
|- ( ( ( # ` W ) = ( N + 1 ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> ( ( ( # ` W ) + 1 ) - 1 ) = ( N + 1 ) ) |
132 |
131
|
3ad2antl2 |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) -> ( ( ( # ` W ) + 1 ) - 1 ) = ( N + 1 ) ) |
133 |
132
|
adantr |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( ( ( # ` W ) + 1 ) - 1 ) = ( N + 1 ) ) |
134 |
123 133
|
eqtrd |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( ( # ` ( W ++ <" Z "> ) ) - 1 ) = ( N + 1 ) ) |
135 |
134
|
oveq2d |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) = ( 0 ..^ ( N + 1 ) ) ) |
136 |
135
|
raleqdv |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E <-> A. i e. ( 0 ..^ ( N + 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) ) |
137 |
119 136
|
mpbird |
|- ( ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ Z e. V ) ) /\ { ( lastS ` W ) , Z } e. E ) -> A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) |
138 |
137
|
exp42 |
|- ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( Z e. V -> ( { ( lastS ` W ) , Z } e. E -> A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) ) ) ) |
139 |
14 138
|
syl |
|- ( W e. ( N WWalksN G ) -> ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( Z e. V -> ( { ( lastS ` W ) , Z } e. E -> A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) ) ) ) |
140 |
139
|
imp41 |
|- ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ { ( lastS ` W ) , Z } e. E ) -> A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) |
141 |
140
|
adantrr |
|- ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E ) |
142 |
|
lswccats1 |
|- ( ( W e. Word V /\ Z e. V ) -> ( lastS ` ( W ++ <" Z "> ) ) = Z ) |
143 |
8 142
|
sylancom |
|- ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> ( lastS ` ( W ++ <" Z "> ) ) = Z ) |
144 |
68
|
3ad2ant1 |
|- ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> 0 < ( N + 1 ) ) |
145 |
70
|
3ad2ant3 |
|- ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( 0 < ( # ` W ) <-> 0 < ( N + 1 ) ) ) |
146 |
144 145
|
mpbird |
|- ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> 0 < ( # ` W ) ) |
147 |
146
|
ad2antlr |
|- ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> 0 < ( # ` W ) ) |
148 |
|
ccatfv0 |
|- ( ( W e. Word V /\ <" Z "> e. Word V /\ 0 < ( # ` W ) ) -> ( ( W ++ <" Z "> ) ` 0 ) = ( W ` 0 ) ) |
149 |
8 10 147 148
|
syl3anc |
|- ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> ( ( W ++ <" Z "> ) ` 0 ) = ( W ` 0 ) ) |
150 |
143 149
|
preq12d |
|- ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } = { Z , ( W ` 0 ) } ) |
151 |
150
|
eleq1d |
|- ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> ( { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E <-> { Z , ( W ` 0 ) } e. E ) ) |
152 |
151
|
biimprcd |
|- ( { Z , ( W ` 0 ) } e. E -> ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) ) |
153 |
152
|
adantl |
|- ( ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) -> ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) -> { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) ) |
154 |
153
|
impcom |
|- ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) |
155 |
13 141 154
|
3jca |
|- ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) ) |
156 |
|
ccatws1len |
|- ( W e. Word ( Vtx ` G ) -> ( # ` ( W ++ <" Z "> ) ) = ( ( # ` W ) + 1 ) ) |
157 |
156
|
3ad2ant2 |
|- ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( # ` ( W ++ <" Z "> ) ) = ( ( # ` W ) + 1 ) ) |
158 |
124
|
3ad2ant3 |
|- ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( # ` W ) + 1 ) = ( ( N + 1 ) + 1 ) ) |
159 |
80 126 126
|
addassd |
|- ( N e. NN0 -> ( ( N + 1 ) + 1 ) = ( N + ( 1 + 1 ) ) ) |
160 |
|
1p1e2 |
|- ( 1 + 1 ) = 2 |
161 |
160
|
oveq2i |
|- ( N + ( 1 + 1 ) ) = ( N + 2 ) |
162 |
159 161
|
eqtrdi |
|- ( N e. NN0 -> ( ( N + 1 ) + 1 ) = ( N + 2 ) ) |
163 |
162
|
3ad2ant1 |
|- ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( N + 1 ) + 1 ) = ( N + 2 ) ) |
164 |
157 158 163
|
3eqtrd |
|- ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( # ` ( W ++ <" Z "> ) ) = ( N + 2 ) ) |
165 |
164
|
ad3antlr |
|- ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> ( # ` ( W ++ <" Z "> ) ) = ( N + 2 ) ) |
166 |
|
2nn |
|- 2 e. NN |
167 |
|
nn0nnaddcl |
|- ( ( N e. NN0 /\ 2 e. NN ) -> ( N + 2 ) e. NN ) |
168 |
166 167
|
mpan2 |
|- ( N e. NN0 -> ( N + 2 ) e. NN ) |
169 |
168
|
3ad2ant1 |
|- ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( N + 2 ) e. NN ) |
170 |
1 2
|
isclwwlknx |
|- ( ( N + 2 ) e. NN -> ( ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) <-> ( ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) /\ ( # ` ( W ++ <" Z "> ) ) = ( N + 2 ) ) ) ) |
171 |
169 170
|
syl |
|- ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) <-> ( ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) /\ ( # ` ( W ++ <" Z "> ) ) = ( N + 2 ) ) ) ) |
172 |
171
|
ad3antlr |
|- ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> ( ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) <-> ( ( ( W ++ <" Z "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" Z "> ) ) - 1 ) ) { ( ( W ++ <" Z "> ) ` i ) , ( ( W ++ <" Z "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( W ++ <" Z "> ) ) , ( ( W ++ <" Z "> ) ` 0 ) } e. E ) /\ ( # ` ( W ++ <" Z "> ) ) = ( N + 2 ) ) ) ) |
173 |
155 165 172
|
mpbir2and |
|- ( ( ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) /\ Z e. V ) /\ ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) ) -> ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) ) |
174 |
173
|
exp31 |
|- ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) -> ( Z e. V -> ( ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) -> ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) ) ) ) |
175 |
3 174
|
mpdan |
|- ( W e. ( N WWalksN G ) -> ( Z e. V -> ( ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) -> ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) ) ) ) |
176 |
175
|
imp |
|- ( ( W e. ( N WWalksN G ) /\ Z e. V ) -> ( ( { ( lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) -> ( W ++ <" Z "> ) e. ( ( N + 2 ) ClWWalksN G ) ) ) |