Step |
Hyp |
Ref |
Expression |
1 |
|
wlkp1.v |
|- V = ( Vtx ` G ) |
2 |
|
wlkp1.i |
|- I = ( iEdg ` G ) |
3 |
|
wlkp1.f |
|- ( ph -> Fun I ) |
4 |
|
wlkp1.a |
|- ( ph -> I e. Fin ) |
5 |
|
wlkp1.b |
|- ( ph -> B e. W ) |
6 |
|
wlkp1.c |
|- ( ph -> C e. V ) |
7 |
|
wlkp1.d |
|- ( ph -> -. B e. dom I ) |
8 |
|
wlkp1.w |
|- ( ph -> F ( Walks ` G ) P ) |
9 |
|
wlkp1.n |
|- N = ( # ` F ) |
10 |
|
wlkp1.e |
|- ( ph -> E e. ( Edg ` G ) ) |
11 |
|
wlkp1.x |
|- ( ph -> { ( P ` N ) , C } C_ E ) |
12 |
|
wlkp1.u |
|- ( ph -> ( iEdg ` S ) = ( I u. { <. B , E >. } ) ) |
13 |
|
wlkp1.h |
|- H = ( F u. { <. N , B >. } ) |
14 |
|
wlkp1.q |
|- Q = ( P u. { <. ( N + 1 ) , C >. } ) |
15 |
|
wlkp1.s |
|- ( ph -> ( Vtx ` S ) = V ) |
16 |
|
fveq2 |
|- ( k = N -> ( Q ` k ) = ( Q ` N ) ) |
17 |
|
fveq2 |
|- ( k = N -> ( P ` k ) = ( P ` N ) ) |
18 |
16 17
|
eqeq12d |
|- ( k = N -> ( ( Q ` k ) = ( P ` k ) <-> ( Q ` N ) = ( P ` N ) ) ) |
19 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
wlkp1lem5 |
|- ( ph -> A. k e. ( 0 ... N ) ( Q ` k ) = ( P ` k ) ) |
20 |
|
wlkcl |
|- ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 ) |
21 |
9
|
eqcomi |
|- ( # ` F ) = N |
22 |
21
|
eleq1i |
|- ( ( # ` F ) e. NN0 <-> N e. NN0 ) |
23 |
|
nn0fz0 |
|- ( N e. NN0 <-> N e. ( 0 ... N ) ) |
24 |
22 23
|
sylbb |
|- ( ( # ` F ) e. NN0 -> N e. ( 0 ... N ) ) |
25 |
8 20 24
|
3syl |
|- ( ph -> N e. ( 0 ... N ) ) |
26 |
18 19 25
|
rspcdva |
|- ( ph -> ( Q ` N ) = ( P ` N ) ) |
27 |
14
|
fveq1i |
|- ( Q ` ( N + 1 ) ) = ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) ) |
28 |
|
ovex |
|- ( N + 1 ) e. _V |
29 |
1 2 3 4 5 6 7 8 9
|
wlkp1lem1 |
|- ( ph -> -. ( N + 1 ) e. dom P ) |
30 |
|
fsnunfv |
|- ( ( ( N + 1 ) e. _V /\ C e. V /\ -. ( N + 1 ) e. dom P ) -> ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) ) = C ) |
31 |
28 6 29 30
|
mp3an2i |
|- ( ph -> ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) ) = C ) |
32 |
27 31
|
syl5eq |
|- ( ph -> ( Q ` ( N + 1 ) ) = C ) |
33 |
26 32
|
preq12d |
|- ( ph -> { ( Q ` N ) , ( Q ` ( N + 1 ) ) } = { ( P ` N ) , C } ) |
34 |
|
fsnunfv |
|- ( ( B e. W /\ E e. ( Edg ` G ) /\ -. B e. dom I ) -> ( ( I u. { <. B , E >. } ) ` B ) = E ) |
35 |
5 10 7 34
|
syl3anc |
|- ( ph -> ( ( I u. { <. B , E >. } ) ` B ) = E ) |
36 |
11 33 35
|
3sstr4d |
|- ( ph -> { ( Q ` N ) , ( Q ` ( N + 1 ) ) } C_ ( ( I u. { <. B , E >. } ) ` B ) ) |
37 |
1 2 3 4 5 6 7 8 9 10 11 12 13
|
wlkp1lem3 |
|- ( ph -> ( ( iEdg ` S ) ` ( H ` N ) ) = ( ( I u. { <. B , E >. } ) ` B ) ) |
38 |
36 37
|
sseqtrrd |
|- ( ph -> { ( Q ` N ) , ( Q ` ( N + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` N ) ) ) |