Step |
Hyp |
Ref |
Expression |
1 |
|
wwlksnredwwlkn.e |
|- E = ( Edg ` G ) |
2 |
1
|
wwlksnredwwlkn |
|- ( N e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) ) |
3 |
2
|
imp |
|- ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) |
4 |
|
simpl |
|- ( ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( W prefix ( N + 1 ) ) = y ) |
5 |
4
|
adantl |
|- ( ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) /\ ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) -> ( W prefix ( N + 1 ) ) = y ) |
6 |
|
fveq1 |
|- ( y = ( W prefix ( N + 1 ) ) -> ( y ` 0 ) = ( ( W prefix ( N + 1 ) ) ` 0 ) ) |
7 |
6
|
eqcoms |
|- ( ( W prefix ( N + 1 ) ) = y -> ( y ` 0 ) = ( ( W prefix ( N + 1 ) ) ` 0 ) ) |
8 |
7
|
adantr |
|- ( ( ( W prefix ( N + 1 ) ) = y /\ ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) ) -> ( y ` 0 ) = ( ( W prefix ( N + 1 ) ) ` 0 ) ) |
9 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
10 |
9 1
|
wwlknp |
|- ( W e. ( ( N + 1 ) WWalksN G ) -> ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) |
11 |
|
nn0p1nn |
|- ( N e. NN0 -> ( N + 1 ) e. NN ) |
12 |
|
peano2nn0 |
|- ( N e. NN0 -> ( N + 1 ) e. NN0 ) |
13 |
|
nn0re |
|- ( ( N + 1 ) e. NN0 -> ( N + 1 ) e. RR ) |
14 |
|
lep1 |
|- ( ( N + 1 ) e. RR -> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) ) |
15 |
12 13 14
|
3syl |
|- ( N e. NN0 -> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) ) |
16 |
|
peano2nn0 |
|- ( ( N + 1 ) e. NN0 -> ( ( N + 1 ) + 1 ) e. NN0 ) |
17 |
16
|
nn0zd |
|- ( ( N + 1 ) e. NN0 -> ( ( N + 1 ) + 1 ) e. ZZ ) |
18 |
|
fznn |
|- ( ( ( N + 1 ) + 1 ) e. ZZ -> ( ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) <-> ( ( N + 1 ) e. NN /\ ( N + 1 ) <_ ( ( N + 1 ) + 1 ) ) ) ) |
19 |
12 17 18
|
3syl |
|- ( N e. NN0 -> ( ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) <-> ( ( N + 1 ) e. NN /\ ( N + 1 ) <_ ( ( N + 1 ) + 1 ) ) ) ) |
20 |
11 15 19
|
mpbir2and |
|- ( N e. NN0 -> ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) ) |
21 |
|
oveq2 |
|- ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( 1 ... ( # ` W ) ) = ( 1 ... ( ( N + 1 ) + 1 ) ) ) |
22 |
21
|
eleq2d |
|- ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( ( N + 1 ) e. ( 1 ... ( # ` W ) ) <-> ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) ) ) |
23 |
20 22
|
syl5ibr |
|- ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N e. NN0 -> ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) |
24 |
23
|
adantl |
|- ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N e. NN0 -> ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) |
25 |
|
simpl |
|- ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> W e. Word ( Vtx ` G ) ) |
26 |
24 25
|
jctild |
|- ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) ) |
27 |
26
|
3adant3 |
|- ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) ) |
28 |
10 27
|
syl |
|- ( W e. ( ( N + 1 ) WWalksN G ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) ) |
29 |
28
|
impcom |
|- ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) |
30 |
29
|
adantl |
|- ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) |
31 |
30
|
adantr |
|- ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) |
32 |
31
|
adantl |
|- ( ( ( W prefix ( N + 1 ) ) = y /\ ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) |
33 |
|
pfxfv0 |
|- ( ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( W ` 0 ) ) |
34 |
32 33
|
syl |
|- ( ( ( W prefix ( N + 1 ) ) = y /\ ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( W ` 0 ) ) |
35 |
|
simprll |
|- ( ( ( W prefix ( N + 1 ) ) = y /\ ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) ) -> ( W ` 0 ) = P ) |
36 |
8 34 35
|
3eqtrd |
|- ( ( ( W prefix ( N + 1 ) ) = y /\ ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) ) -> ( y ` 0 ) = P ) |
37 |
36
|
ex |
|- ( ( W prefix ( N + 1 ) ) = y -> ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) -> ( y ` 0 ) = P ) ) |
38 |
37
|
adantr |
|- ( ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) -> ( y ` 0 ) = P ) ) |
39 |
38
|
impcom |
|- ( ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) /\ ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) -> ( y ` 0 ) = P ) |
40 |
|
simpr |
|- ( ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> { ( lastS ` y ) , ( lastS ` W ) } e. E ) |
41 |
40
|
adantl |
|- ( ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) /\ ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) -> { ( lastS ` y ) , ( lastS ` W ) } e. E ) |
42 |
5 39 41
|
3jca |
|- ( ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) /\ ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) -> ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) |
43 |
42
|
ex |
|- ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) -> ( ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) ) |
44 |
43
|
reximdva |
|- ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) -> ( E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) ) |
45 |
44
|
ex |
|- ( ( W ` 0 ) = P -> ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) ) ) |
46 |
45
|
com13 |
|- ( E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( ( W ` 0 ) = P -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) ) ) |
47 |
3 46
|
mpcom |
|- ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( ( W ` 0 ) = P -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) ) |
48 |
29 33
|
syl |
|- ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( W ` 0 ) ) |
49 |
48
|
eqcomd |
|- ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( W ` 0 ) = ( ( W prefix ( N + 1 ) ) ` 0 ) ) |
50 |
49
|
adantl |
|- ( ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) -> ( W ` 0 ) = ( ( W prefix ( N + 1 ) ) ` 0 ) ) |
51 |
|
fveq1 |
|- ( ( W prefix ( N + 1 ) ) = y -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( y ` 0 ) ) |
52 |
51
|
adantr |
|- ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( y ` 0 ) ) |
53 |
52
|
adantr |
|- ( ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( y ` 0 ) ) |
54 |
|
simpr |
|- ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) -> ( y ` 0 ) = P ) |
55 |
54
|
adantr |
|- ( ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) -> ( y ` 0 ) = P ) |
56 |
50 53 55
|
3eqtrd |
|- ( ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) -> ( W ` 0 ) = P ) |
57 |
56
|
ex |
|- ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) -> ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( W ` 0 ) = P ) ) |
58 |
57
|
3adant3 |
|- ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( W ` 0 ) = P ) ) |
59 |
58
|
com12 |
|- ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( W ` 0 ) = P ) ) |
60 |
59
|
rexlimdvw |
|- ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( W ` 0 ) = P ) ) |
61 |
47 60
|
impbid |
|- ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( ( W ` 0 ) = P <-> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) ) |