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

Metamath Proof Explorer

Theorem wwlksnredwwlkn

Description: For each walk (as word) of length at least 1 there is a shorter walk (as word). (Contributed by Alexander van der Vekens, 22-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 26-Oct-2022)

Ref Expression
Hypothesis wwlksnredwwlkn.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion wwlksnredwwlkn ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 wwlksnredwwlkn.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
2 eqidd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) = ( 𝑊 prefix ( 𝑁 + 1 ) ) )
3 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4 3 1 wwlknp ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
5 simprl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
6 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
7 peano2nn0 ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 )
8 6 7 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 )
9 id ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
10 nn0p1nn ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ )
11 6 10 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ )
12 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
13 id ⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℝ )
14 peano2re ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ∈ ℝ )
15 peano2re ⊢ ( ( 𝑁 + 1 ) ∈ ℝ → ( ( 𝑁 + 1 ) + 1 ) ∈ ℝ )
16 14 15 syl ⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 + 1 ) + 1 ) ∈ ℝ )
17 13 14 16 3jca ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 ∈ ℝ ∧ ( 𝑁 + 1 ) ∈ ℝ ∧ ( ( 𝑁 + 1 ) + 1 ) ∈ ℝ ) )
18 12 17 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ℝ ∧ ( 𝑁 + 1 ) ∈ ℝ ∧ ( ( 𝑁 + 1 ) + 1 ) ∈ ℝ ) )
19 12 ltp1d ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 < ( 𝑁 + 1 ) )
20 nn0re ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℝ )
21 6 20 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℝ )
22 21 ltp1d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) < ( ( 𝑁 + 1 ) + 1 ) )
23 lttr ⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 + 1 ) ∈ ℝ ∧ ( ( 𝑁 + 1 ) + 1 ) ∈ ℝ ) → ( ( 𝑁 < ( 𝑁 + 1 ) ∧ ( 𝑁 + 1 ) < ( ( 𝑁 + 1 ) + 1 ) ) → 𝑁 < ( ( 𝑁 + 1 ) + 1 ) ) )
24 23 imp ⊢ ( ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 + 1 ) ∈ ℝ ∧ ( ( 𝑁 + 1 ) + 1 ) ∈ ℝ ) ∧ ( 𝑁 < ( 𝑁 + 1 ) ∧ ( 𝑁 + 1 ) < ( ( 𝑁 + 1 ) + 1 ) ) ) → 𝑁 < ( ( 𝑁 + 1 ) + 1 ) )
25 18 19 22 24 syl12anc ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 < ( ( 𝑁 + 1 ) + 1 ) )
26 elfzo0 ⊢ ( 𝑁 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) + 1 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ ∧ 𝑁 < ( ( 𝑁 + 1 ) + 1 ) ) )
27 9 11 25 26 syl3anbrc ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) + 1 ) ) )
28 fz0add1fz1 ⊢ ( ( ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 ∧ 𝑁 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑁 + 1 ) ∈ ( 1 ... ( ( 𝑁 + 1 ) + 1 ) ) )
29 8 27 28 syl2anc ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( 1 ... ( ( 𝑁 + 1 ) + 1 ) ) )
30 29 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑁 + 1 ) ∈ ( 1 ... ( ( 𝑁 + 1 ) + 1 ) ) )
31 oveq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 1 ... ( ♯ ‘ 𝑊 ) ) = ( 1 ... ( ( 𝑁 + 1 ) + 1 ) ) )
32 31 eleq2d ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 1 ... ( ( 𝑁 + 1 ) + 1 ) ) ) )
33 32 adantl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 1 ... ( ( 𝑁 + 1 ) + 1 ) ) ) )
34 33 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 1 ... ( ( 𝑁 + 1 ) + 1 ) ) ) )
35 30 34 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
36 5 35 jca ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) )
37 36 3adantr3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) )
38 pfxfvlsw ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) )
39 37 38 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) → ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) )
40 lsw ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
41 40 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
42 41 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
43 39 42 preq12d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } = { ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) , ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) } )
44 oveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) )
45 44 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) )
46 45 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) )
47 46 fveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) ) )
48 47 preq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) → { ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) , ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) } = { ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) , ( 𝑊 ‘ ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) ) } )
49 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
50 1cnd ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
51 49 50 pncand ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
52 51 fveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) = ( 𝑊 ‘ 𝑁 ) )
53 6 nn0cnd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
54 53 50 pncand ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) )
55 54 fveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ‘ ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) ) = ( 𝑊 ‘ ( 𝑁 + 1 ) ) )
56 52 55 preq12d ⊢ ( 𝑁 ∈ ℕ0 → { ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) , ( 𝑊 ‘ ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) ) } = { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } )
57 56 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) → { ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) , ( 𝑊 ‘ ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) ) } = { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } )
58 48 57 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) → { ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) , ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) } = { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } )
59 fveq2 ⊢ ( 𝑖 = 𝑁 → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 𝑁 ) )
60 fvoveq1 ⊢ ( 𝑖 = 𝑁 → ( 𝑊 ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑁 + 1 ) ) )
61 59 60 preq12d ⊢ ( 𝑖 = 𝑁 → { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } )
62 61 eleq1d ⊢ ( 𝑖 = 𝑁 → ( { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
63 62 rspcv ⊢ ( 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
64 fzonn0p1 ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
65 63 64 syl11 ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → ( 𝑁 ∈ ℕ0 → { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
66 65 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( 𝑁 ∈ ℕ0 → { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 ) )
67 66 impcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) → { ( 𝑊 ‘ 𝑁 ) , ( 𝑊 ‘ ( 𝑁 + 1 ) ) } ∈ 𝐸 )
68 58 67 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) → { ( 𝑊 ‘ ( ( 𝑁 + 1 ) − 1 ) ) , ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) } ∈ 𝐸 )
69 43 68 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 )
70 4 69 sylan2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 )
71 wwlksnred ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) )
72 71 imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) )
73 eqeq2 ⊢ ( 𝑦 = ( 𝑊 prefix ( 𝑁 + 1 ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ↔ ( 𝑊 prefix ( 𝑁 + 1 ) ) = ( 𝑊 prefix ( 𝑁 + 1 ) ) ) )
74 fveq2 ⊢ ( 𝑦 = ( 𝑊 prefix ( 𝑁 + 1 ) ) → ( lastS ‘ 𝑦 ) = ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) )
75 74 preq1d ⊢ ( 𝑦 = ( 𝑊 prefix ( 𝑁 + 1 ) ) → { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } = { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } )
76 75 eleq1d ⊢ ( 𝑦 = ( 𝑊 prefix ( 𝑁 + 1 ) ) → ( { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ↔ { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) )
77 73 76 anbi12d ⊢ ( 𝑦 = ( 𝑊 prefix ( 𝑁 + 1 ) ) → ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ↔ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = ( 𝑊 prefix ( 𝑁 + 1 ) ) ∧ { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )
78 77 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ∧ 𝑦 = ( 𝑊 prefix ( 𝑁 + 1 ) ) ) → ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ↔ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = ( 𝑊 prefix ( 𝑁 + 1 ) ) ∧ { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )
79 72 78 rspcedv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = ( 𝑊 prefix ( 𝑁 + 1 ) ) ∧ { ( lastS ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) → ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )
80 2 70 79 mp2and ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) )
81 80 ex ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )