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 ‘ 𝐺 ) = ∅ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 WWalksN 𝐺 ) = ∅ )

Proof

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