Step |
Hyp |
Ref |
Expression |
1 |
|
0wlk.v |
|- V = ( Vtx ` G ) |
2 |
|
1fv |
|- ( ( N e. V /\ P = { <. 0 , N >. } ) -> ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) ) |
3 |
2
|
ancoms |
|- ( ( P = { <. 0 , N >. } /\ N e. V ) -> ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) ) |
4 |
3
|
simpld |
|- ( ( P = { <. 0 , N >. } /\ N e. V ) -> P : ( 0 ... 0 ) --> V ) |
5 |
1
|
1vgrex |
|- ( N e. V -> G e. _V ) |
6 |
5
|
adantl |
|- ( ( P = { <. 0 , N >. } /\ N e. V ) -> G e. _V ) |
7 |
1
|
0wlk |
|- ( G e. _V -> ( (/) ( Walks ` G ) P <-> P : ( 0 ... 0 ) --> V ) ) |
8 |
6 7
|
syl |
|- ( ( P = { <. 0 , N >. } /\ N e. V ) -> ( (/) ( Walks ` G ) P <-> P : ( 0 ... 0 ) --> V ) ) |
9 |
4 8
|
mpbird |
|- ( ( P = { <. 0 , N >. } /\ N e. V ) -> (/) ( Walks ` G ) P ) |