Metamath Proof Explorer


Theorem wspn0

Description: If there are no vertices, then there are no simple paths (of any length), too. (Contributed by Alexander van der Vekens, 11-Mar-2018) (Revised by AV, 16-May-2021) (Proof shortened by AV, 13-Mar-2022)

Ref Expression
Hypothesis wspn0.v V = Vtx G
Assertion wspn0 V = N WSPathsN G =

Proof

Step Hyp Ref Expression
1 wspn0.v V = Vtx G
2 wspthsn N WSPathsN G = w N WWalksN G | f f SPaths G w
3 wwlknbp1 w N WWalksN G N 0 w 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 Word Vtx G w Word
8 0wrd0 w Word w =
9 7 8 syl6bb V = w Word Vtx G w =
10 fveq2 w = w =
11 hash0 = 0
12 10 11 syl6eq w = w = 0
13 12 eqeq1d w = w = N + 1 0 = N + 1
14 13 adantl N 0 w = w = N + 1 0 = N + 1
15 nn0p1gt0 N 0 0 < N + 1
16 15 gt0ne0d N 0 N + 1 0
17 eqneqall N + 1 = 0 N + 1 0 ¬ f f SPaths G w
18 17 eqcoms 0 = N + 1 N + 1 0 ¬ f f SPaths G w
19 16 18 syl5com N 0 0 = N + 1 ¬ f f SPaths G w
20 19 adantr N 0 w = 0 = N + 1 ¬ f f SPaths G w
21 14 20 sylbid N 0 w = w = N + 1 ¬ f f SPaths G w
22 21 expcom w = N 0 w = N + 1 ¬ f f SPaths G w
23 22 com23 w = w = N + 1 N 0 ¬ f f SPaths G w
24 9 23 syl6bi V = w Word Vtx G w = N + 1 N 0 ¬ f f SPaths G w
25 24 com14 N 0 w Word Vtx G w = N + 1 V = ¬ f f SPaths G w
26 25 3imp N 0 w Word Vtx G w = N + 1 V = ¬ f f SPaths G w
27 3 26 syl w N WWalksN G V = ¬ f f SPaths G w
28 27 impcom V = w N WWalksN G ¬ f f SPaths G w
29 28 ralrimiva V = w N WWalksN G ¬ f f SPaths G w
30 rabeq0 w N WWalksN G | f f SPaths G w = w N WWalksN G ¬ f f SPaths G w
31 29 30 sylibr V = w N WWalksN G | f f SPaths G w =
32 2 31 syl5eq V = N WSPathsN G =