Metamath Proof Explorer


Theorem wwlksnwwlksnon

Description: A walk of fixed length is a walk of fixed length between two vertices. (Contributed by Alexander van der Vekens, 21-Feb-2018) (Revised by AV, 12-May-2021) (Revised by AV, 13-Mar-2022)

Ref Expression
Hypothesis wwlksnwwlksnon.v 𝑉 = ( Vtx ‘ 𝐺 )
Assertion wwlksnwwlksnon ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ∃ 𝑎𝑉𝑏𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) )

Proof

Step Hyp Ref Expression
1 wwlksnwwlksnon.v 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlknbp1 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) )
3 1 eqcomi ( Vtx ‘ 𝐺 ) = 𝑉
4 3 wrdeqi Word ( Vtx ‘ 𝐺 ) = Word 𝑉
5 4 eleq2i ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ↔ 𝑊 ∈ Word 𝑉 )
6 5 biimpi ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → 𝑊 ∈ Word 𝑉 )
7 6 3ad2ant2 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑊 ∈ Word 𝑉 )
8 nn0p1nn ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
9 lbfzo0 ( 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑁 + 1 ) ∈ ℕ )
10 8 9 sylibr ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
11 10 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
12 oveq2 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
13 12 eleq2d ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
14 13 3ad2ant3 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
15 11 14 mpbird ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
16 15 adantl ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
17 wrdsymbcl ( ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
18 7 16 17 syl2an2 ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
19 fzonn0p1 ( 𝑁 ∈ ℕ0𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
20 19 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
21 12 eleq2d ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
22 21 3ad2ant3 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
23 20 22 mpbird ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
24 wrdsymbcl ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊𝑁 ) ∈ 𝑉 )
25 7 23 24 syl2anc ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑊𝑁 ) ∈ 𝑉 )
26 25 adantl ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑊𝑁 ) ∈ 𝑉 )
27 simpl ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) )
28 eqidd ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) )
29 eqidd ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑊𝑁 ) = ( 𝑊𝑁 ) )
30 eqeq2 ( 𝑎 = ( 𝑊 ‘ 0 ) → ( ( 𝑊 ‘ 0 ) = 𝑎 ↔ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ) )
31 30 3anbi2d ( 𝑎 = ( 𝑊 ‘ 0 ) → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊𝑁 ) = 𝑏 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊𝑁 ) = 𝑏 ) ) )
32 eqeq2 ( 𝑏 = ( 𝑊𝑁 ) → ( ( 𝑊𝑁 ) = 𝑏 ↔ ( 𝑊𝑁 ) = ( 𝑊𝑁 ) ) )
33 32 3anbi3d ( 𝑏 = ( 𝑊𝑁 ) → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊𝑁 ) = 𝑏 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊𝑁 ) = ( 𝑊𝑁 ) ) ) )
34 31 33 rspc2ev ( ( ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑊𝑁 ) ∈ 𝑉 ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊𝑁 ) = ( 𝑊𝑁 ) ) ) → ∃ 𝑎𝑉𝑏𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊𝑁 ) = 𝑏 ) )
35 18 26 27 28 29 34 syl113anc ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ∃ 𝑎𝑉𝑏𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊𝑁 ) = 𝑏 ) )
36 2 35 mpdan ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ∃ 𝑎𝑉𝑏𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊𝑁 ) = 𝑏 ) )
37 simp1 ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊𝑁 ) = 𝑏 ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) )
38 37 a1i ( ( 𝑎𝑉𝑏𝑉 ) → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊𝑁 ) = 𝑏 ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
39 38 rexlimivv ( ∃ 𝑎𝑉𝑏𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊𝑁 ) = 𝑏 ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) )
40 36 39 impbii ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ∃ 𝑎𝑉𝑏𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊𝑁 ) = 𝑏 ) )
41 wwlknon ( 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊𝑁 ) = 𝑏 ) )
42 41 bicomi ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊𝑁 ) = 𝑏 ) ↔ 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) )
43 42 2rexbii ( ∃ 𝑎𝑉𝑏𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊𝑁 ) = 𝑏 ) ↔ ∃ 𝑎𝑉𝑏𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) )
44 40 43 bitri ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ∃ 𝑎𝑉𝑏𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) )