This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion wspn0 ( 𝑉 = ∅ → ( 𝑁 WSPathsN 𝐺 ) = ∅ )

Proof

Step Hyp Ref Expression
1 wspn0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wspthsn ⊢ ( 𝑁 WSPathsN 𝐺 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 }
3 wwlknbp1 ⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) )
4 1 eqeq1i ⊢ ( 𝑉 = ∅ ↔ ( Vtx ‘ 𝐺 ) = ∅ )
5 wrdeq ⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → Word ( Vtx ‘ 𝐺 ) = Word ∅ )
6 4 5 sylbi ⊢ ( 𝑉 = ∅ → Word ( Vtx ‘ 𝐺 ) = Word ∅ )
7 6 eleq2d ⊢ ( 𝑉 = ∅ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ↔ 𝑤 ∈ Word ∅ ) )
8 0wrd0 ⊢ ( 𝑤 ∈ Word ∅ ↔ 𝑤 = ∅ )
9 7 8 bitrdi ⊢ ( 𝑉 = ∅ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ↔ 𝑤 = ∅ ) )
10 fveq2 ⊢ ( 𝑤 = ∅ → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ∅ ) )
11 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
12 10 11 eqtrdi ⊢ ( 𝑤 = ∅ → ( ♯ ‘ 𝑤 ) = 0 )
13 12 eqeq1d ⊢ ( 𝑤 = ∅ → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ↔ 0 = ( 𝑁 + 1 ) ) )
14 13 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑤 = ∅ ) → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ↔ 0 = ( 𝑁 + 1 ) ) )
15 nn0p1gt0 ⊢ ( 𝑁 ∈ ℕ0 → 0 < ( 𝑁 + 1 ) )
16 15 gt0ne0d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ≠ 0 )
17 eqneqall ⊢ ( ( 𝑁 + 1 ) = 0 → ( ( 𝑁 + 1 ) ≠ 0 → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
18 17 eqcoms ⊢ ( 0 = ( 𝑁 + 1 ) → ( ( 𝑁 + 1 ) ≠ 0 → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
19 16 18 syl5com ⊢ ( 𝑁 ∈ ℕ0 → ( 0 = ( 𝑁 + 1 ) → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
20 19 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑤 = ∅ ) → ( 0 = ( 𝑁 + 1 ) → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
21 14 20 sylbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑤 = ∅ ) → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
22 21 expcom ⊢ ( 𝑤 = ∅ → ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) ) )
23 22 com23 ⊢ ( 𝑤 = ∅ → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ0 → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) ) )
24 9 23 biimtrdi ⊢ ( 𝑉 = ∅ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ0 → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) ) ) )
25 24 com14 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ( 𝑉 = ∅ → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) ) ) )
26 25 3imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) → ( 𝑉 = ∅ → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
27 3 26 syl ⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑉 = ∅ → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
28 27 impcom ⊢ ( ( 𝑉 = ∅ ∧ 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 )
29 28 ralrimiva ⊢ ( 𝑉 = ∅ → ∀ 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 )
30 rabeq0 ⊢ ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 } = ∅ ↔ ∀ 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 )
31 29 30 sylibr ⊢ ( 𝑉 = ∅ → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 } = ∅ )
32 2 31 eqtrid ⊢ ( 𝑉 = ∅ → ( 𝑁 WSPathsN 𝐺 ) = ∅ )