Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
2 |
1
|
wwlknbp |
|- ( W e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ W e. Word ( Vtx ` G ) ) ) |
3 |
|
iswwlksn |
|- ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) ) |
4 |
3
|
3ad2ant2 |
|- ( ( G e. _V /\ N e. NN0 /\ W e. Word ( Vtx ` G ) ) -> ( W e. ( N WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) ) |
5 |
|
simpl |
|- ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> W e. ( WWalks ` G ) ) |
6 |
4 5
|
syl6bi |
|- ( ( G e. _V /\ N e. NN0 /\ W e. Word ( Vtx ` G ) ) -> ( W e. ( N WWalksN G ) -> W e. ( WWalks ` G ) ) ) |
7 |
2 6
|
mpcom |
|- ( W e. ( N WWalksN G ) -> W e. ( WWalks ` G ) ) |