Metamath Proof Explorer

Theorem 0enwwlksnge1

Description: In graphs without edges, there are no walks of length greater than 0. (Contributed by Alexander van der Vekens, 26-Jul-2018) (Revised by AV, 7-May-2021)

Ref Expression
Assertion 0enwwlksnge1 ⊢ Edg ⁡ G = ∅ ∧ N ∈ ℕ → N WWalksN G = ∅

Proof

Step Hyp Ref Expression
1 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
2 wwlksn ⊢ N ∈ ℕ 0 → N WWalksN G = w ∈ WWalks ⁡ G | w = N + 1
3 1 2 syl ⊢ N ∈ ℕ → N WWalksN G = w ∈ WWalks ⁡ G | w = N + 1
4 3 adantl ⊢ Edg ⁡ G = ∅ ∧ N ∈ ℕ → N WWalksN G = w ∈ WWalks ⁡ G | w = N + 1
5 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
6 eqid ⊢ Edg ⁡ G = Edg ⁡ G
7 5 6 iswwlks ⊢ w ∈ WWalks ⁡ G ↔ w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G
8 nncn ⊢ N ∈ ℕ → N ∈ ℂ
9 pncan1 ⊢ N ∈ ℂ → N + 1 - 1 = N
10 8 9 syl ⊢ N ∈ ℕ → N + 1 - 1 = N
11 id ⊢ N ∈ ℕ → N ∈ ℕ
12 10 11 eqeltrd ⊢ N ∈ ℕ → N + 1 - 1 ∈ ℕ
13 12 adantl ⊢ Edg ⁡ G = ∅ ∧ N ∈ ℕ → N + 1 - 1 ∈ ℕ
14 13 adantl ⊢ w = N + 1 ∧ Edg ⁡ G = ∅ ∧ N ∈ ℕ → N + 1 - 1 ∈ ℕ
15 oveq1 ⊢ w = N + 1 → w − 1 = N + 1 - 1
16 15 eleq1d ⊢ w = N + 1 → w − 1 ∈ ℕ ↔ N + 1 - 1 ∈ ℕ
17 16 adantr ⊢ w = N + 1 ∧ Edg ⁡ G = ∅ ∧ N ∈ ℕ → w − 1 ∈ ℕ ↔ N + 1 - 1 ∈ ℕ
18 14 17 mpbird ⊢ w = N + 1 ∧ Edg ⁡ G = ∅ ∧ N ∈ ℕ → w − 1 ∈ ℕ
19 lbfzo0 ⊢ 0 ∈ 0 ..^ w − 1 ↔ w − 1 ∈ ℕ
20 18 19 sylibr ⊢ w = N + 1 ∧ Edg ⁡ G = ∅ ∧ N ∈ ℕ → 0 ∈ 0 ..^ w − 1
21 fveq2 ⊢ i = 0 → w ⁡ i = w ⁡ 0
22 fv0p1e1 ⊢ i = 0 → w ⁡ i + 1 = w ⁡ 1
23 21 22 preq12d ⊢ i = 0 → w ⁡ i w ⁡ i + 1 = w ⁡ 0 w ⁡ 1
24 23 eleq1d ⊢ i = 0 → w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ↔ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G
25 24 adantl ⊢ w = N + 1 ∧ Edg ⁡ G = ∅ ∧ N ∈ ℕ ∧ i = 0 → w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ↔ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G
26 20 25 rspcdv ⊢ w = N + 1 ∧ Edg ⁡ G = ∅ ∧ N ∈ ℕ → ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G → w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G
27 eleq2 ⊢ Edg ⁡ G = ∅ → w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ↔ w ⁡ 0 w ⁡ 1 ∈ ∅
28 noel ⊢ ¬ w ⁡ 0 w ⁡ 1 ∈ ∅
29 28 pm2.21i ⊢ w ⁡ 0 w ⁡ 1 ∈ ∅ → ¬ w = N + 1
30 27 29 biimtrdi ⊢ Edg ⁡ G = ∅ → w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G → ¬ w = N + 1
31 30 adantr ⊢ Edg ⁡ G = ∅ ∧ N ∈ ℕ → w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G → ¬ w = N + 1
32 31 adantl ⊢ w = N + 1 ∧ Edg ⁡ G = ∅ ∧ N ∈ ℕ → w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G → ¬ w = N + 1
33 26 32 syldc ⊢ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G → w = N + 1 ∧ Edg ⁡ G = ∅ ∧ N ∈ ℕ → ¬ w = N + 1
34 33 3ad2ant3 ⊢ w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G → w = N + 1 ∧ Edg ⁡ G = ∅ ∧ N ∈ ℕ → ¬ w = N + 1
35 34 com12 ⊢ w = N + 1 ∧ Edg ⁡ G = ∅ ∧ N ∈ ℕ → w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G → ¬ w = N + 1
36 7 35 biimtrid ⊢ w = N + 1 ∧ Edg ⁡ G = ∅ ∧ N ∈ ℕ → w ∈ WWalks ⁡ G → ¬ w = N + 1
37 36 expimpd ⊢ w = N + 1 → Edg ⁡ G = ∅ ∧ N ∈ ℕ ∧ w ∈ WWalks ⁡ G → ¬ w = N + 1
38 ax-1 ⊢ ¬ w = N + 1 → Edg ⁡ G = ∅ ∧ N ∈ ℕ ∧ w ∈ WWalks ⁡ G → ¬ w = N + 1
39 37 38 pm2.61i ⊢ Edg ⁡ G = ∅ ∧ N ∈ ℕ ∧ w ∈ WWalks ⁡ G → ¬ w = N + 1
40 39 ralrimiva ⊢ Edg ⁡ G = ∅ ∧ N ∈ ℕ → ∀ w ∈ WWalks ⁡ G ¬ w = N + 1
41 rabeq0 ⊢ w ∈ WWalks ⁡ G | w = N + 1 = ∅ ↔ ∀ w ∈ WWalks ⁡ G ¬ w = N + 1
42 40 41 sylibr ⊢ Edg ⁡ G = ∅ ∧ N ∈ ℕ → w ∈ WWalks ⁡ G | w = N + 1 = ∅
43 4 42 eqtrd ⊢ Edg ⁡ G = ∅ ∧ N ∈ ℕ → N WWalksN G = ∅