Metamath Proof Explorer

Theorem wwlksnextproplem3

Description: Lemma 3 for wwlksnextprop . (Contributed by Alexander van der Vekens, 1-Aug-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 29-Oct-2022)

Ref Expression
Hypotheses wwlksnextprop.x ⊢ 𝑋 = ( ( 𝑁 + 1 ) WWalksN 𝐺 )
wwlksnextprop.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
wwlksnextprop.y ⊢ 𝑌 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 }
Assertion wwlksnextproplem3 ( ( 𝑊 ∈ 𝑋 ∧ ( 𝑊 ‘ 0 ) = 𝑃 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ 𝑌 )

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x ⊢ 𝑋 = ( ( 𝑁 + 1 ) WWalksN 𝐺 )
2 wwlksnextprop.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 wwlksnextprop.y ⊢ 𝑌 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 }
4 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
5 iswwlksn ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) )
6 4 5 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) )
7 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
8 7 wwlkbp ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) )
9 lencl ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
10 eqcom ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ↔ ( ( 𝑁 + 1 ) + 1 ) = ( ♯ ‘ 𝑊 ) )
11 nn0cn ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
12 11 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
13 1cnd ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 1 ∈ ℂ )
14 nn0cn ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
15 4 14 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
16 15 adantl ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℂ )
17 subadd2 ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝑁 + 1 ) ∈ ℂ ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) = ( 𝑁 + 1 ) ↔ ( ( 𝑁 + 1 ) + 1 ) = ( ♯ ‘ 𝑊 ) ) )
18 17 bicomd ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝑁 + 1 ) ∈ ℂ ) → ( ( ( 𝑁 + 1 ) + 1 ) = ( ♯ ‘ 𝑊 ) ↔ ( ( ♯ ‘ 𝑊 ) − 1 ) = ( 𝑁 + 1 ) ) )
19 12 13 16 18 syl3anc ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑁 + 1 ) + 1 ) = ( ♯ ‘ 𝑊 ) ↔ ( ( ♯ ‘ 𝑊 ) − 1 ) = ( 𝑁 + 1 ) ) )
20 10 19 syl5bb ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ↔ ( ( ♯ ‘ 𝑊 ) − 1 ) = ( 𝑁 + 1 ) ) )
21 eqcom ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) = ( 𝑁 + 1 ) ↔ ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
22 21 biimpi ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) = ( 𝑁 + 1 ) → ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
23 20 22 syl6bi ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
24 23 ex ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) )
25 24 com23 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) )
26 9 25 syl ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) )
27 8 26 simpl2im ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) )
28 27 imp31 ⊢ ( ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
29 28 oveq2d ⊢ ( ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) = ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
30 simpll ⊢ ( ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → 𝑊 ∈ ( WWalks ‘ 𝐺 ) )
31 nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
32 2re ⊢ 2 ∈ ℝ
33 32 a1i ⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ )
34 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
35 33 34 addge02d ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ≤ 𝑁 ↔ 2 ≤ ( 𝑁 + 2 ) ) )
36 31 35 mpbid ⊢ ( 𝑁 ∈ ℕ0 → 2 ≤ ( 𝑁 + 2 ) )
37 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
38 1cnd ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
39 37 38 38 addassd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + ( 1 + 1 ) ) )
40 1p1e2 ⊢ ( 1 + 1 ) = 2
41 40 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 1 + 1 ) = 2 )
42 41 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + ( 1 + 1 ) ) = ( 𝑁 + 2 ) )
43 39 42 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + 2 ) )
44 36 43 breqtrrd ⊢ ( 𝑁 ∈ ℕ0 → 2 ≤ ( ( 𝑁 + 1 ) + 1 ) )
45 44 adantl ⊢ ( ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → 2 ≤ ( ( 𝑁 + 1 ) + 1 ) )
46 breq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 2 ≤ ( ♯ ‘ 𝑊 ) ↔ 2 ≤ ( ( 𝑁 + 1 ) + 1 ) ) )
47 46 ad2antlr ⊢ ( ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 2 ≤ ( ♯ ‘ 𝑊 ) ↔ 2 ≤ ( ( 𝑁 + 1 ) + 1 ) ) )
48 45 47 mpbird ⊢ ( ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → 2 ≤ ( ♯ ‘ 𝑊 ) )
49 wwlksm1edg ⊢ ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ ( WWalks ‘ 𝐺 ) )
50 30 48 49 syl2anc ⊢ ( ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ ( WWalks ‘ 𝐺 ) )
51 29 50 eqeltrd ⊢ ( ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) )
52 51 expcom ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ) )
53 6 52 sylbid ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ) )
54 53 com12 ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ) )
55 54 adantr ⊢ ( ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑃 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ) )
56 55 imp ⊢ ( ( ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑃 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) )
57 7 2 wwlknp ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
58 simpll ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
59 peano2nn0 ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 )
60 4 59 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 )
61 peano2re ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ∈ ℝ )
62 34 61 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℝ )
63 62 lep1d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) )
64 elfz2nn0 ⊢ ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ↔ ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 ∧ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) )
65 4 60 63 64 syl3anbrc ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) )
66 65 adantl ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) )
67 oveq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 0 ... ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) )
68 67 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 0 ... ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) )
69 66 68 eleqtrrd ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
70 69 adantll ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
71 58 70 jca ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )
72 71 ex ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) )
73 72 3adant3 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) )
74 57 73 syl ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) )
75 74 adantr ⊢ ( ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑃 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) )
76 75 imp ⊢ ( ( ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑃 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )
77 pfxlen ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
78 76 77 syl ⊢ ( ( ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑃 ) ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
79 56 78 jca ⊢ ( ( ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑃 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) ) )
80 iswwlksn ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) ) ) )
81 80 adantl ⊢ ( ( ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑃 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) ) ) )
82 79 81 mpbird ⊢ ( ( ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑃 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) )
83 82 exp31 ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( ( 𝑊 ‘ 0 ) = 𝑃 → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) ) )
84 83 1 eleq2s ⊢ ( 𝑊 ∈ 𝑋 → ( ( 𝑊 ‘ 0 ) = 𝑃 → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) ) )
85 84 3imp ⊢ ( ( 𝑊 ∈ 𝑋 ∧ ( 𝑊 ‘ 0 ) = 𝑃 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) )
86 1 wwlksnextproplem1 ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
87 86 3adant2 ⊢ ( ( 𝑊 ∈ 𝑋 ∧ ( 𝑊 ‘ 0 ) = 𝑃 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
88 simp2 ⊢ ( ( 𝑊 ∈ 𝑋 ∧ ( 𝑊 ‘ 0 ) = 𝑃 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 ‘ 0 ) = 𝑃 )
89 87 88 eqtrd ⊢ ( ( 𝑊 ∈ 𝑋 ∧ ( 𝑊 ‘ 0 ) = 𝑃 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑃 )
90 fveq1 ⊢ ( 𝑤 = ( 𝑊 prefix ( 𝑁 + 1 ) ) → ( 𝑤 ‘ 0 ) = ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) )
91 90 eqeq1d ⊢ ( 𝑤 = ( 𝑊 prefix ( 𝑁 + 1 ) ) → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑃 ) )
92 91 3 elrab2 ⊢ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ 𝑌 ↔ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑃 ) )
93 85 89 92 sylanbrc ⊢ ( ( 𝑊 ∈ 𝑋 ∧ ( 𝑊 ‘ 0 ) = 𝑃 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ 𝑌 )