Step |
Hyp |
Ref |
Expression |
1 |
|
iswwlksnx.v |
|- V = ( Vtx ` G ) |
2 |
|
iswwlksnx.e |
|- E = ( Edg ` G ) |
3 |
|
iswwlksn |
|- ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) ) |
4 |
1 2
|
iswwlks |
|- ( W e. ( WWalks ` G ) <-> ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) |
5 |
|
df-3an |
|- ( ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) <-> ( ( W =/= (/) /\ W e. Word V ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) |
6 |
|
nn0p1gt0 |
|- ( N e. NN0 -> 0 < ( N + 1 ) ) |
7 |
6
|
gt0ne0d |
|- ( N e. NN0 -> ( N + 1 ) =/= 0 ) |
8 |
7
|
adantr |
|- ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( N + 1 ) =/= 0 ) |
9 |
|
neeq1 |
|- ( ( # ` W ) = ( N + 1 ) -> ( ( # ` W ) =/= 0 <-> ( N + 1 ) =/= 0 ) ) |
10 |
9
|
adantl |
|- ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( ( # ` W ) =/= 0 <-> ( N + 1 ) =/= 0 ) ) |
11 |
8 10
|
mpbird |
|- ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( # ` W ) =/= 0 ) |
12 |
|
hasheq0 |
|- ( W e. Word V -> ( ( # ` W ) = 0 <-> W = (/) ) ) |
13 |
12
|
necon3bid |
|- ( W e. Word V -> ( ( # ` W ) =/= 0 <-> W =/= (/) ) ) |
14 |
11 13
|
syl5ibcom |
|- ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( W e. Word V -> W =/= (/) ) ) |
15 |
14
|
pm4.71rd |
|- ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( W e. Word V <-> ( W =/= (/) /\ W e. Word V ) ) ) |
16 |
15
|
bicomd |
|- ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( ( W =/= (/) /\ W e. Word V ) <-> W e. Word V ) ) |
17 |
16
|
anbi1d |
|- ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( ( ( W =/= (/) /\ W e. Word V ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) ) |
18 |
5 17
|
syl5bb |
|- ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) ) |
19 |
4 18
|
syl5bb |
|- ( ( N e. NN0 /\ ( # ` W ) = ( N + 1 ) ) -> ( W e. ( WWalks ` G ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) ) |
20 |
19
|
ex |
|- ( N e. NN0 -> ( ( # ` W ) = ( N + 1 ) -> ( W e. ( WWalks ` G ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) ) ) |
21 |
20
|
pm5.32rd |
|- ( N e. NN0 -> ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( # ` W ) = ( N + 1 ) ) ) ) |
22 |
|
df-3an |
|- ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ ( # ` W ) = ( N + 1 ) ) <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) /\ ( # ` W ) = ( N + 1 ) ) ) |
23 |
21 22
|
bitr4di |
|- ( N e. NN0 -> ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ ( # ` W ) = ( N + 1 ) ) ) ) |
24 |
3 23
|
bitrd |
|- ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ ( # ` W ) = ( N + 1 ) ) ) ) |