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 |
13
|
a1i |
|- ( ph -> H = ( F u. { <. N , B >. } ) ) |
15 |
14
|
fveq1d |
|- ( ph -> ( H ` N ) = ( ( F u. { <. N , B >. } ) ` N ) ) |
16 |
9
|
fvexi |
|- N e. _V |
17 |
2
|
wlkf |
|- ( F ( Walks ` G ) P -> F e. Word dom I ) |
18 |
|
lencl |
|- ( F e. Word dom I -> ( # ` F ) e. NN0 ) |
19 |
|
wrddm |
|- ( F e. Word dom I -> dom F = ( 0 ..^ ( # ` F ) ) ) |
20 |
|
fzonel |
|- -. ( # ` F ) e. ( 0 ..^ ( # ` F ) ) |
21 |
9
|
a1i |
|- ( ( ( # ` F ) e. NN0 /\ dom F = ( 0 ..^ ( # ` F ) ) ) -> N = ( # ` F ) ) |
22 |
|
simpr |
|- ( ( ( # ` F ) e. NN0 /\ dom F = ( 0 ..^ ( # ` F ) ) ) -> dom F = ( 0 ..^ ( # ` F ) ) ) |
23 |
21 22
|
eleq12d |
|- ( ( ( # ` F ) e. NN0 /\ dom F = ( 0 ..^ ( # ` F ) ) ) -> ( N e. dom F <-> ( # ` F ) e. ( 0 ..^ ( # ` F ) ) ) ) |
24 |
20 23
|
mtbiri |
|- ( ( ( # ` F ) e. NN0 /\ dom F = ( 0 ..^ ( # ` F ) ) ) -> -. N e. dom F ) |
25 |
18 19 24
|
syl2anc |
|- ( F e. Word dom I -> -. N e. dom F ) |
26 |
8 17 25
|
3syl |
|- ( ph -> -. N e. dom F ) |
27 |
|
fsnunfv |
|- ( ( N e. _V /\ B e. W /\ -. N e. dom F ) -> ( ( F u. { <. N , B >. } ) ` N ) = B ) |
28 |
16 5 26 27
|
mp3an2i |
|- ( ph -> ( ( F u. { <. N , B >. } ) ` N ) = B ) |
29 |
15 28
|
eqtrd |
|- ( ph -> ( H ` N ) = B ) |
30 |
12 29
|
fveq12d |
|- ( ph -> ( ( iEdg ` S ) ` ( H ` N ) ) = ( ( I u. { <. B , E >. } ) ` B ) ) |