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 bitrdi ⊢ V = ∅ → w ∈ 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 ∈ ℕ 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 = ∅