Metamath Proof Explorer

Theorem wwlksnextwrd

Description: Lemma for wwlksnextbij . (Contributed by Alexander van der Vekens, 5-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 27-Oct-2022)

Ref Expression
Hypotheses wwlksnextbij0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wwlksnextbij0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
wwlksnextbij0.d ⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) }
Assertion wwlksnextwrd ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝐷 = { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } )

Proof

Step Hyp Ref Expression
1 wwlksnextbij0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlksnextbij0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 wwlksnextbij0.d ⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) }
4 3anass ⊢ ( ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ↔ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) )
5 4 bianass ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) ↔ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) )
6 1 wwlknbp ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) )
7 simpl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) ) → 𝑁 ∈ ℕ0 )
8 simpl ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) → 𝑤 ∈ Word 𝑉 )
9 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
10 2re ⊢ 2 ∈ ℝ
11 10 a1i ⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ )
12 nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
13 2pos ⊢ 0 < 2
14 13 a1i ⊢ ( 𝑁 ∈ ℕ0 → 0 < 2 )
15 9 11 12 14 addgegt0d ⊢ ( 𝑁 ∈ ℕ0 → 0 < ( 𝑁 + 2 ) )
16 15 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) → 0 < ( 𝑁 + 2 ) )
17 breq2 ⊢ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) → ( 0 < ( ♯ ‘ 𝑤 ) ↔ 0 < ( 𝑁 + 2 ) ) )
18 17 ad2antll ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) → ( 0 < ( ♯ ‘ 𝑤 ) ↔ 0 < ( 𝑁 + 2 ) ) )
19 16 18 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) → 0 < ( ♯ ‘ 𝑤 ) )
20 hashgt0n0 ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑤 ) ) → 𝑤 ≠ ∅ )
21 8 19 20 syl2an2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) → 𝑤 ≠ ∅ )
22 lswcl ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ 𝑤 ≠ ∅ ) → ( lastS ‘ 𝑤 ) ∈ 𝑉 )
23 8 21 22 syl2an2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) → ( lastS ‘ 𝑤 ) ∈ 𝑉 )
24 23 adantrr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) ) → ( lastS ‘ 𝑤 ) ∈ 𝑉 )
25 pfxcl ⊢ ( 𝑤 ∈ Word 𝑉 → ( 𝑤 prefix ( 𝑁 + 1 ) ) ∈ Word 𝑉 )
26 eleq1 ⊢ ( 𝑊 = ( 𝑤 prefix ( 𝑁 + 1 ) ) → ( 𝑊 ∈ Word 𝑉 ↔ ( 𝑤 prefix ( 𝑁 + 1 ) ) ∈ Word 𝑉 ) )
27 25 26 imbitrrid ⊢ ( 𝑊 = ( 𝑤 prefix ( 𝑁 + 1 ) ) → ( 𝑤 ∈ Word 𝑉 → 𝑊 ∈ Word 𝑉 ) )
28 27 eqcoms ⊢ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 → ( 𝑤 ∈ Word 𝑉 → 𝑊 ∈ Word 𝑉 ) )
29 28 adantr ⊢ ( ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) → ( 𝑤 ∈ Word 𝑉 → 𝑊 ∈ Word 𝑉 ) )
30 29 com12 ⊢ ( 𝑤 ∈ Word 𝑉 → ( ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) → 𝑊 ∈ Word 𝑉 ) )
31 30 adantr ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) → ( ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) → 𝑊 ∈ Word 𝑉 ) )
32 31 imp ⊢ ( ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) → 𝑊 ∈ Word 𝑉 )
33 32 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) ) → 𝑊 ∈ Word 𝑉 )
34 oveq1 ⊢ ( 𝑊 = ( 𝑤 prefix ( 𝑁 + 1 ) ) → ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) = ( ( 𝑤 prefix ( 𝑁 + 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) )
35 34 eqcoms ⊢ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 → ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) = ( ( 𝑤 prefix ( 𝑁 + 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) )
36 35 adantr ⊢ ( ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) → ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) = ( ( 𝑤 prefix ( 𝑁 + 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) )
37 36 ad2antll ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) ) → ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) = ( ( 𝑤 prefix ( 𝑁 + 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) )
38 oveq1 ⊢ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) → ( ( ♯ ‘ 𝑤 ) − 1 ) = ( ( 𝑁 + 2 ) − 1 ) )
39 38 adantl ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) → ( ( ♯ ‘ 𝑤 ) − 1 ) = ( ( 𝑁 + 2 ) − 1 ) )
40 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
41 2cnd ⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℂ )
42 1cnd ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
43 40 41 42 addsubassd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 2 ) − 1 ) = ( 𝑁 + ( 2 − 1 ) ) )
44 2m1e1 ⊢ ( 2 − 1 ) = 1
45 44 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 2 − 1 ) = 1 )
46 45 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + ( 2 − 1 ) ) = ( 𝑁 + 1 ) )
47 43 46 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 2 ) − 1 ) = ( 𝑁 + 1 ) )
48 39 47 sylan9eqr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) → ( ( ♯ ‘ 𝑤 ) − 1 ) = ( 𝑁 + 1 ) )
49 48 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) → ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) = ( 𝑤 prefix ( 𝑁 + 1 ) ) )
50 49 oveq1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) → ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) = ( ( 𝑤 prefix ( 𝑁 + 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) )
51 pfxlswccat ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ 𝑤 ≠ ∅ ) → ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) = 𝑤 )
52 8 21 51 syl2an2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) → ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) = 𝑤 )
53 50 52 eqtr3d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) → ( ( 𝑤 prefix ( 𝑁 + 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) = 𝑤 )
54 53 adantrr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) ) → ( ( 𝑤 prefix ( 𝑁 + 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) = 𝑤 )
55 37 54 eqtr2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) ) → 𝑤 = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) )
56 simprrr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) ) → { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 )
57 1 2 wwlksnextbi ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( lastS ‘ 𝑤 ) ∈ 𝑉 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑤 = ( 𝑊 ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) → ( 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
58 7 24 33 55 56 57 syl23anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) ) → ( 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
59 58 exbiri ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) )
60 59 com23 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) → 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) )
61 60 3ad2ant2 ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) → 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) )
62 6 61 mpcom ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) → 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) )
63 62 expcomd ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) → ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) → 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) )
64 63 imp ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) → ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) → 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) )
65 1 2 wwlknp ⊢ ( 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
66 40 42 42 addassd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + ( 1 + 1 ) ) )
67 1p1e2 ⊢ ( 1 + 1 ) = 2
68 67 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 1 + 1 ) = 2 )
69 68 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + ( 1 + 1 ) ) = ( 𝑁 + 2 ) )
70 66 69 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + 2 ) )
71 70 eqeq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑤 ) = ( ( 𝑁 + 1 ) + 1 ) ↔ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) )
72 71 biimpd ⊢ ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑤 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) )
73 72 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) → ( ( ♯ ‘ 𝑤 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) )
74 73 com12 ⊢ ( ( ♯ ‘ 𝑤 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) → ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) )
75 74 adantl ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) → ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) )
76 simpl ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( ( 𝑁 + 1 ) + 1 ) ) → 𝑤 ∈ Word 𝑉 )
77 75 76 jctild ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) → ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) )
78 77 3adant3 ⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) → ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) )
79 65 78 syl ⊢ ( 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) → ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) )
80 79 com12 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) → ( 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) )
81 80 3adant1 ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) → ( 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) )
82 6 81 syl ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) )
83 82 adantr ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) → ( 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ) )
84 64 83 impbid ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) → ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ↔ 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) )
85 84 ex ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) → ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ↔ 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) )
86 85 pm5.32rd ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) ↔ ( 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) ) )
87 5 86 bitrid ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑤 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) ↔ ( 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ) ) )
88 87 rabbidva2 ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } = { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } )
89 3 88 eqtrid ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝐷 = { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } )