Step |
Hyp |
Ref |
Expression |
1 |
|
wspn0.v |
|- V = ( Vtx ` G ) |
2 |
|
wspthsn |
|- ( N WSPathsN G ) = { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w } |
3 |
|
wwlknbp1 |
|- ( w e. ( N WWalksN G ) -> ( N e. NN0 /\ w e. Word ( Vtx ` G ) /\ ( # ` w ) = ( N + 1 ) ) ) |
4 |
1
|
eqeq1i |
|- ( V = (/) <-> ( Vtx ` G ) = (/) ) |
5 |
|
wrdeq |
|- ( ( Vtx ` G ) = (/) -> Word ( Vtx ` G ) = Word (/) ) |
6 |
4 5
|
sylbi |
|- ( V = (/) -> Word ( Vtx ` G ) = Word (/) ) |
7 |
6
|
eleq2d |
|- ( V = (/) -> ( w e. Word ( Vtx ` G ) <-> w e. Word (/) ) ) |
8 |
|
0wrd0 |
|- ( w e. Word (/) <-> w = (/) ) |
9 |
7 8
|
syl6bb |
|- ( V = (/) -> ( w e. Word ( Vtx ` G ) <-> w = (/) ) ) |
10 |
|
fveq2 |
|- ( w = (/) -> ( # ` w ) = ( # ` (/) ) ) |
11 |
|
hash0 |
|- ( # ` (/) ) = 0 |
12 |
10 11
|
eqtrdi |
|- ( w = (/) -> ( # ` w ) = 0 ) |
13 |
12
|
eqeq1d |
|- ( w = (/) -> ( ( # ` w ) = ( N + 1 ) <-> 0 = ( N + 1 ) ) ) |
14 |
13
|
adantl |
|- ( ( N e. NN0 /\ w = (/) ) -> ( ( # ` w ) = ( N + 1 ) <-> 0 = ( N + 1 ) ) ) |
15 |
|
nn0p1gt0 |
|- ( N e. NN0 -> 0 < ( N + 1 ) ) |
16 |
15
|
gt0ne0d |
|- ( N e. NN0 -> ( N + 1 ) =/= 0 ) |
17 |
|
eqneqall |
|- ( ( N + 1 ) = 0 -> ( ( N + 1 ) =/= 0 -> -. E. f f ( SPaths ` G ) w ) ) |
18 |
17
|
eqcoms |
|- ( 0 = ( N + 1 ) -> ( ( N + 1 ) =/= 0 -> -. E. f f ( SPaths ` G ) w ) ) |
19 |
16 18
|
syl5com |
|- ( N e. NN0 -> ( 0 = ( N + 1 ) -> -. E. f f ( SPaths ` G ) w ) ) |
20 |
19
|
adantr |
|- ( ( N e. NN0 /\ w = (/) ) -> ( 0 = ( N + 1 ) -> -. E. f f ( SPaths ` G ) w ) ) |
21 |
14 20
|
sylbid |
|- ( ( N e. NN0 /\ w = (/) ) -> ( ( # ` w ) = ( N + 1 ) -> -. E. f f ( SPaths ` G ) w ) ) |
22 |
21
|
expcom |
|- ( w = (/) -> ( N e. NN0 -> ( ( # ` w ) = ( N + 1 ) -> -. E. f f ( SPaths ` G ) w ) ) ) |
23 |
22
|
com23 |
|- ( w = (/) -> ( ( # ` w ) = ( N + 1 ) -> ( N e. NN0 -> -. E. f f ( SPaths ` G ) w ) ) ) |
24 |
9 23
|
syl6bi |
|- ( V = (/) -> ( w e. Word ( Vtx ` G ) -> ( ( # ` w ) = ( N + 1 ) -> ( N e. NN0 -> -. E. f f ( SPaths ` G ) w ) ) ) ) |
25 |
24
|
com14 |
|- ( N e. NN0 -> ( w e. Word ( Vtx ` G ) -> ( ( # ` w ) = ( N + 1 ) -> ( V = (/) -> -. E. f f ( SPaths ` G ) w ) ) ) ) |
26 |
25
|
3imp |
|- ( ( N e. NN0 /\ w e. Word ( Vtx ` G ) /\ ( # ` w ) = ( N + 1 ) ) -> ( V = (/) -> -. E. f f ( SPaths ` G ) w ) ) |
27 |
3 26
|
syl |
|- ( w e. ( N WWalksN G ) -> ( V = (/) -> -. E. f f ( SPaths ` G ) w ) ) |
28 |
27
|
impcom |
|- ( ( V = (/) /\ w e. ( N WWalksN G ) ) -> -. E. f f ( SPaths ` G ) w ) |
29 |
28
|
ralrimiva |
|- ( V = (/) -> A. w e. ( N WWalksN G ) -. E. f f ( SPaths ` G ) w ) |
30 |
|
rabeq0 |
|- ( { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w } = (/) <-> A. w e. ( N WWalksN G ) -. E. f f ( SPaths ` G ) w ) |
31 |
29 30
|
sylibr |
|- ( V = (/) -> { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w } = (/) ) |
32 |
2 31
|
syl5eq |
|- ( V = (/) -> ( N WSPathsN G ) = (/) ) |