Metamath Proof Explorer

Theorem clwwlkel

Description: Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by AV, 28-Sep-2018) (Revised by AV, 25-Apr-2021)

Ref Expression
Hypothesis clwwlkf1o.d ⊢ 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
Assertion clwwlkel ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 clwwlkf1o.d ⊢ 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
2 ccatws1n0 ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ≠ ∅ )
3 2 adantr ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) → ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ≠ ∅ )
4 3 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ≠ ∅ )
5 simprl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
6 fstwrdne0 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
7 6 s1cld ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
8 ccatcl ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ Word ( Vtx ‘ 𝐺 ) )
9 5 7 8 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ Word ( Vtx ‘ 𝐺 ) )
10 9 3adant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ Word ( Vtx ‘ 𝐺 ) )
11 5 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
12 7 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
13 elfzonn0 ⊢ ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → 𝑖 ∈ ℕ0 )
14 13 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℕ0 )
15 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
16 15 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℤ )
17 elfzo0 ⊢ ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ↔ ( 𝑖 ∈ ℕ0 ∧ ( 𝑁 − 1 ) ∈ ℕ ∧ 𝑖 < ( 𝑁 − 1 ) ) )
18 nn0re ⊢ ( 𝑖 ∈ ℕ0 → 𝑖 ∈ ℝ )
19 18 adantr ⊢ ( ( 𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → 𝑖 ∈ ℝ )
20 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
21 peano2rem ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
22 20 21 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℝ )
23 22 adantl ⊢ ( ( 𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) ∈ ℝ )
24 20 adantl ⊢ ( ( 𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
25 19 23 24 3jca ⊢ ( ( 𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑖 ∈ ℝ ∧ ( 𝑁 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
26 25 adantr ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ∧ 𝑖 < ( 𝑁 − 1 ) ) → ( 𝑖 ∈ ℝ ∧ ( 𝑁 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
27 20 ltm1d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) < 𝑁 )
28 27 adantl ⊢ ( ( 𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) < 𝑁 )
29 28 anim1ci ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ∧ 𝑖 < ( 𝑁 − 1 ) ) → ( 𝑖 < ( 𝑁 − 1 ) ∧ ( 𝑁 − 1 ) < 𝑁 ) )
30 lttr ⊢ ( ( 𝑖 ∈ ℝ ∧ ( 𝑁 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑖 < ( 𝑁 − 1 ) ∧ ( 𝑁 − 1 ) < 𝑁 ) → 𝑖 < 𝑁 ) )
31 26 29 30 sylc ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ∧ 𝑖 < ( 𝑁 − 1 ) ) → 𝑖 < 𝑁 )
32 31 ex ⊢ ( ( 𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑖 < ( 𝑁 − 1 ) → 𝑖 < 𝑁 ) )
33 32 impancom ⊢ ( ( 𝑖 ∈ ℕ0 ∧ 𝑖 < ( 𝑁 − 1 ) ) → ( 𝑁 ∈ ℕ → 𝑖 < 𝑁 ) )
34 33 3adant2 ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( 𝑁 − 1 ) ∈ ℕ ∧ 𝑖 < ( 𝑁 − 1 ) ) → ( 𝑁 ∈ ℕ → 𝑖 < 𝑁 ) )
35 17 34 sylbi ⊢ ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → ( 𝑁 ∈ ℕ → 𝑖 < 𝑁 ) )
36 35 impcom ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑖 < 𝑁 )
37 elfzo0z ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁 ) )
38 14 16 36 37 syl3anbrc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑁 ) )
39 38 adantlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑁 ) )
40 oveq2 ⊢ ( ( ♯ ‘ 𝑃 ) = 𝑁 → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ..^ 𝑁 ) )
41 40 eleq2d ⊢ ( ( ♯ ‘ 𝑃 ) = 𝑁 → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ↔ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) )
42 41 ad2antll ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ↔ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) )
43 42 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ↔ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) )
44 39 43 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
45 ccatval1 ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) )
46 11 12 44 45 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) )
47 elfzom1p1elfzo ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑁 ) )
48 47 adantlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ 𝑁 ) )
49 40 ad2antll ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ..^ 𝑁 ) )
50 49 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ..^ 𝑁 ) )
51 48 50 eleqtrrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
52 ccatval1 ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
53 11 12 51 52 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
54 46 53 preq12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } )
55 54 eleq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
56 55 ralbidva ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
57 56 biimprcd ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
58 57 adantr ⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
59 58 expdcom ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
60 59 3imp ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
61 fzo0end ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
62 40 eleq2d ⊢ ( ( ♯ ‘ 𝑃 ) = 𝑁 → ( ( 𝑁 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ↔ ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) )
63 62 adantl ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) → ( ( 𝑁 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ↔ ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) )
64 61 63 syl5ibrcom ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) → ( 𝑁 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ) )
65 64 imp ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( 𝑁 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
66 ccatval1 ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑁 − 1 ) ) = ( 𝑃 ‘ ( 𝑁 − 1 ) ) )
67 5 7 65 66 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑁 − 1 ) ) = ( 𝑃 ‘ ( 𝑁 − 1 ) ) )
68 lsw ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
69 68 adantr ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
70 fvoveq1 ⊢ ( ( ♯ ‘ 𝑃 ) = 𝑁 → ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 𝑃 ‘ ( 𝑁 − 1 ) ) )
71 70 adantl ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) → ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 𝑃 ‘ ( 𝑁 − 1 ) ) )
72 69 71 eqtr2d ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) → ( 𝑃 ‘ ( 𝑁 − 1 ) ) = ( lastS ‘ 𝑃 ) )
73 72 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( 𝑃 ‘ ( 𝑁 − 1 ) ) = ( lastS ‘ 𝑃 ) )
74 67 73 eqtr2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( lastS ‘ 𝑃 ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑁 − 1 ) ) )
75 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
76 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
77 75 76 npcand ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
78 77 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑁 ) )
79 78 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑁 ) )
80 fveq2 ⊢ ( ( ♯ ‘ 𝑃 ) = 𝑁 → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ♯ ‘ 𝑃 ) ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑁 ) )
81 80 ad2antll ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ♯ ‘ 𝑃 ) ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑁 ) )
82 ccatws1ls ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ♯ ‘ 𝑃 ) ) = ( 𝑃 ‘ 0 ) )
83 5 6 82 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ♯ ‘ 𝑃 ) ) = ( 𝑃 ‘ 0 ) )
84 79 81 83 3eqtr2rd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( 𝑃 ‘ 0 ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
85 74 84 preq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } = { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑁 − 1 ) ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) } )
86 85 eleq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑁 − 1 ) ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
87 86 biimpcd ⊢ ( { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑁 − 1 ) ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
88 87 adantl ⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑁 − 1 ) ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
89 88 expdcom ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑁 − 1 ) ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
90 89 3imp ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑁 − 1 ) ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
91 ovex ⊢ ( 𝑁 − 1 ) ∈ V
92 fveq2 ⊢ ( 𝑖 = ( 𝑁 − 1 ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑁 − 1 ) ) )
93 fvoveq1 ⊢ ( 𝑖 = ( 𝑁 − 1 ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
94 92 93 preq12d ⊢ ( 𝑖 = ( 𝑁 − 1 ) → { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑁 − 1 ) ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) } )
95 94 eleq1d ⊢ ( 𝑖 = ( 𝑁 − 1 ) → ( { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑁 − 1 ) ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
96 91 95 ralsn ⊢ ( ∀ 𝑖 ∈ { ( 𝑁 − 1 ) } { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑁 − 1 ) ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
97 90 96 sylibr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ∀ 𝑖 ∈ { ( 𝑁 − 1 ) } { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
98 75 76 76 addsubd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) − 1 ) = ( ( 𝑁 − 1 ) + 1 ) )
99 98 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ..^ ( ( 𝑁 − 1 ) + 1 ) ) )
100 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
101 elnn0uz ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 ↔ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
102 100 101 sylib ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
103 fzosplitsn ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 0 ..^ ( 𝑁 − 1 ) ) ∪ { ( 𝑁 − 1 ) } ) )
104 102 103 syl ⊢ ( 𝑁 ∈ ℕ → ( 0 ..^ ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 0 ..^ ( 𝑁 − 1 ) ) ∪ { ( 𝑁 − 1 ) } ) )
105 99 104 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) = ( ( 0 ..^ ( 𝑁 − 1 ) ) ∪ { ( 𝑁 − 1 ) } ) )
106 105 raleqdv ⊢ ( 𝑁 ∈ ℕ → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( ( 0 ..^ ( 𝑁 − 1 ) ) ∪ { ( 𝑁 − 1 ) } ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
107 ralunb ⊢ ( ∀ 𝑖 ∈ ( ( 0 ..^ ( 𝑁 − 1 ) ) ∪ { ( 𝑁 − 1 ) } ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ { ( 𝑁 − 1 ) } { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
108 106 107 bitrdi ⊢ ( 𝑁 ∈ ℕ → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ { ( 𝑁 − 1 ) } { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
109 108 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ { ( 𝑁 − 1 ) } { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
110 60 97 109 mpbir2and ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
111 ccatlen ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) )
112 5 7 111 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) )
113 id ⊢ ( ( ♯ ‘ 𝑃 ) = 𝑁 → ( ♯ ‘ 𝑃 ) = 𝑁 )
114 s1len ⊢ ( ♯ ‘ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) = 1
115 114 a1i ⊢ ( ( ♯ ‘ 𝑃 ) = 𝑁 → ( ♯ ‘ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) = 1 )
116 113 115 oveq12d ⊢ ( ( ♯ ‘ 𝑃 ) = 𝑁 → ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑁 + 1 ) )
117 116 ad2antll ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑁 + 1 ) )
118 112 117 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑁 + 1 ) )
119 118 3adant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑁 + 1 ) )
120 119 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
121 120 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) − 1 ) ) = ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) )
122 121 raleqdv ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
123 110 122 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
124 4 10 123 3jca ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
125 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
126 iswwlksn ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑁 + 1 ) ) ) )
127 125 126 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑁 + 1 ) ) ) )
128 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
129 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
130 128 129 iswwlks ⊢ ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
131 130 anbi1i ⊢ ( ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑁 + 1 ) ) ↔ ( ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑁 + 1 ) ) )
132 127 131 bitrdi ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑁 + 1 ) ) ) )
133 132 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑁 + 1 ) ) ) )
134 124 119 133 mpbir2and ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) )
135 lswccats1 ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ) → ( lastS ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑃 ‘ 0 ) )
136 5 6 135 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( lastS ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑃 ‘ 0 ) )
137 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ℕ )
138 137 biimpri ⊢ ( 𝑁 ∈ ℕ → 0 ∈ ( 0 ..^ 𝑁 ) )
139 40 eleq2d ⊢ ( ( ♯ ‘ 𝑃 ) = 𝑁 → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ↔ 0 ∈ ( 0 ..^ 𝑁 ) ) )
140 139 adantl ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ↔ 0 ∈ ( 0 ..^ 𝑁 ) ) )
141 138 140 syl5ibrcom ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ) )
142 141 imp ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
143 ccatval1 ⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑃 ‘ 0 ) )
144 5 7 142 143 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑃 ‘ 0 ) )
145 136 144 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ) → ( lastS ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 0 ) )
146 145 3adant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( lastS ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 0 ) )
147 fveq2 ⊢ ( 𝑤 = ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) → ( lastS ‘ 𝑤 ) = ( lastS ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) )
148 fveq1 ⊢ ( 𝑤 = ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) → ( 𝑤 ‘ 0 ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 0 ) )
149 147 148 eqeq12d ⊢ ( 𝑤 = ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) → ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ↔ ( lastS ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 0 ) ) )
150 149 1 elrab2 ⊢ ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ 𝐷 ↔ ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 0 ) ) )
151 134 146 150 sylanbrc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ∈ 𝐷 )