Metamath Proof Explorer

Theorem numclwlk2lem2f

Description: R is a function mapping the "closed (n+2)-walks v(0) ... v(n-2) v(n-1) v(n) v(n+1) v(n+2) starting at X = v(0) = v(n+2) with v(n) =/= X" to the words representing the prefix v(0) ... v(n-2) v(n-1) v(n) of the walk. (Contributed by Alexander van der Vekens, 5-Oct-2018) (Revised by AV, 31-May-2021) (Proof shortened by AV, 23-Mar-2022) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses numclwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
numclwwlk.q ⊢ 𝑄 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
numclwwlk.h ⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
numclwwlk.r ⊢ 𝑅 = ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↦ ( 𝑥 prefix ( 𝑁 + 1 ) ) )
Assertion numclwlk2lem2f ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑅 : ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ⟶ ( 𝑋 𝑄 𝑁 ) )

Proof

Step Hyp Ref Expression
1 numclwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 numclwwlk.q ⊢ 𝑄 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
3 numclwwlk.h ⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
4 numclwwlk.r ⊢ 𝑅 = ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↦ ( 𝑥 prefix ( 𝑁 + 1 ) ) )
5 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
6 2z ⊢ 2 ∈ ℤ
7 6 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℤ )
8 nn0pzuz ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ∈ ℤ ) → ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) )
9 5 7 8 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) )
10 9 anim2i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) ) )
11 10 3adant1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) ) )
12 3 numclwwlkovh ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐻 ( 𝑁 + 2 ) ) = { 𝑤 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } )
13 12 eleq2d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↔ 𝑥 ∈ { 𝑤 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } ) )
14 11 13 syl ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↔ 𝑥 ∈ { 𝑤 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } ) )
15 fveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ‘ 0 ) = ( 𝑥 ‘ 0 ) )
16 15 eqeq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ‘ 0 ) = 𝑋 ↔ ( 𝑥 ‘ 0 ) = 𝑋 ) )
17 fveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) = ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) )
18 17 15 neeq12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ↔ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) )
19 16 18 anbi12d ⊢ ( 𝑤 = 𝑥 → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) ↔ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) )
20 19 elrab ⊢ ( 𝑥 ∈ { 𝑤 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } ↔ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) )
21 14 20 bitrdi ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↔ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) )
22 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
23 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
24 23 7 zaddcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 2 ) ∈ ℤ )
25 uzid ⊢ ( ( 𝑁 + 2 ) ∈ ℤ → ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ ( 𝑁 + 2 ) ) )
26 24 25 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ ( 𝑁 + 2 ) ) )
27 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
28 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
29 27 28 28 addassd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + ( 1 + 1 ) ) )
30 1p1e2 ⊢ ( 1 + 1 ) = 2
31 30 a1i ⊢ ( 𝑁 ∈ ℕ → ( 1 + 1 ) = 2 )
32 31 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + ( 1 + 1 ) ) = ( 𝑁 + 2 ) )
33 29 32 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + 2 ) )
34 33 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( ℤ≥ ‘ ( ( 𝑁 + 1 ) + 1 ) ) = ( ℤ≥ ‘ ( 𝑁 + 2 ) ) )
35 26 34 eleqtrrd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ ( ( 𝑁 + 1 ) + 1 ) ) )
36 22 35 jca ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ ( ( 𝑁 + 1 ) + 1 ) ) ) )
37 36 3ad2ant3 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ ( ( 𝑁 + 1 ) + 1 ) ) ) )
38 37 adantr ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → ( ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ ( ( 𝑁 + 1 ) + 1 ) ) ) )
39 simprl ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) )
40 wwlksubclwwlk ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) → ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( ( ( 𝑁 + 1 ) − 1 ) WWalksN 𝐺 ) ) )
41 38 39 40 sylc ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( ( ( 𝑁 + 1 ) − 1 ) WWalksN 𝐺 ) )
42 pncan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
43 42 eqcomd ⊢ ( 𝑁 ∈ ℂ → 𝑁 = ( ( 𝑁 + 1 ) − 1 ) )
44 27 43 syl ⊢ ( 𝑁 ∈ ℕ → 𝑁 = ( ( 𝑁 + 1 ) − 1 ) )
45 44 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 WWalksN 𝐺 ) = ( ( ( 𝑁 + 1 ) − 1 ) WWalksN 𝐺 ) )
46 45 eleq2d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( ( ( 𝑁 + 1 ) − 1 ) WWalksN 𝐺 ) ) )
47 46 3ad2ant3 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( ( ( 𝑁 + 1 ) − 1 ) WWalksN 𝐺 ) ) )
48 47 adantr ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( ( ( 𝑁 + 1 ) − 1 ) WWalksN 𝐺 ) ) )
49 41 48 mpbird ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) )
50 1 clwwlknbp ⊢ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ) )
51 simprl ⊢ ( ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) → ( 𝑥 ‘ 0 ) = 𝑋 )
52 simprr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ) → 𝑥 ∈ Word 𝑉 )
53 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
54 5 53 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ0 )
55 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
56 55 lep1d ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≤ ( 𝑁 + 1 ) )
57 elfz2nn0 ⊢ ( 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝑁 + 1 ) ) )
58 5 54 56 57 syl3anbrc ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
59 2cnd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
60 addsubass ⊢ ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 2 ) − 1 ) = ( 𝑁 + ( 2 − 1 ) ) )
61 2m1e1 ⊢ ( 2 − 1 ) = 1
62 61 oveq2i ⊢ ( 𝑁 + ( 2 − 1 ) ) = ( 𝑁 + 1 )
63 60 62 eqtrdi ⊢ ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 2 ) − 1 ) = ( 𝑁 + 1 ) )
64 27 59 28 63 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 2 ) − 1 ) = ( 𝑁 + 1 ) )
65 64 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 0 ... ( ( 𝑁 + 2 ) − 1 ) ) = ( 0 ... ( 𝑁 + 1 ) ) )
66 58 65 eleqtrrd ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 0 ... ( ( 𝑁 + 2 ) − 1 ) ) )
67 elfzp1b ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑁 + 2 ) ∈ ℤ ) → ( 𝑁 ∈ ( 0 ... ( ( 𝑁 + 2 ) − 1 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 1 ... ( 𝑁 + 2 ) ) ) )
68 23 24 67 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ( 0 ... ( ( 𝑁 + 2 ) − 1 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 1 ... ( 𝑁 + 2 ) ) ) )
69 66 68 mpbid ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ( 1 ... ( 𝑁 + 2 ) ) )
70 69 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ) → ( 𝑁 + 1 ) ∈ ( 1 ... ( 𝑁 + 2 ) ) )
71 oveq2 ⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) → ( 1 ... ( ♯ ‘ 𝑥 ) ) = ( 1 ... ( 𝑁 + 2 ) ) )
72 71 eleq2d ⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) → ( ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑥 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 1 ... ( 𝑁 + 2 ) ) ) )
73 72 ad2antrl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ) → ( ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑥 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 1 ... ( 𝑁 + 2 ) ) ) )
74 70 73 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ) → ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑥 ) ) )
75 pfxfv0 ⊢ ( ( 𝑥 ∈ Word 𝑉 ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑥 ) ) ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑥 ‘ 0 ) )
76 52 74 75 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑥 ‘ 0 ) )
77 76 ex ⊢ ( 𝑁 ∈ ℕ → ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑥 ‘ 0 ) ) )
78 77 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑥 ‘ 0 ) ) )
79 78 impcom ⊢ ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑥 ‘ 0 ) )
80 79 ad2antrl ⊢ ( ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑥 ‘ 0 ) )
81 simpl ⊢ ( ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → ( 𝑥 ‘ 0 ) = 𝑋 )
82 80 81 eqtrd ⊢ ( ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 )
83 pfxfvlsw ⊢ ( ( 𝑥 ∈ Word 𝑉 ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑥 ) ) ) → ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) = ( 𝑥 ‘ ( ( 𝑁 + 1 ) − 1 ) ) )
84 52 74 83 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ) → ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) = ( 𝑥 ‘ ( ( 𝑁 + 1 ) − 1 ) ) )
85 27 42 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
86 27 59 pncand ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 2 ) − 2 ) = 𝑁 )
87 85 86 eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) − 1 ) = ( ( 𝑁 + 2 ) − 2 ) )
88 87 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ‘ ( ( 𝑁 + 1 ) − 1 ) ) = ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) )
89 88 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ) → ( 𝑥 ‘ ( ( 𝑁 + 1 ) − 1 ) ) = ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) )
90 84 89 eqtr2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ) → ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) = ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) )
91 90 ex ⊢ ( 𝑁 ∈ ℕ → ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) → ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) = ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ) )
92 91 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) → ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) = ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ) )
93 92 impcom ⊢ ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) = ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) )
94 93 neeq1d ⊢ ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ↔ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ ( 𝑥 ‘ 0 ) ) )
95 94 biimpcd ⊢ ( ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) → ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ ( 𝑥 ‘ 0 ) ) )
96 95 adantl ⊢ ( ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) → ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ ( 𝑥 ‘ 0 ) ) )
97 96 impcom ⊢ ( ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) → ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ ( 𝑥 ‘ 0 ) )
98 97 adantl ⊢ ( ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ ( 𝑥 ‘ 0 ) )
99 neeq2 ⊢ ( 𝑋 = ( 𝑥 ‘ 0 ) → ( ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ↔ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ ( 𝑥 ‘ 0 ) ) )
100 99 eqcoms ⊢ ( ( 𝑥 ‘ 0 ) = 𝑋 → ( ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ↔ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ ( 𝑥 ‘ 0 ) ) )
101 100 adantr ⊢ ( ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → ( ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ↔ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ ( 𝑥 ‘ 0 ) ) )
102 98 101 mpbird ⊢ ( ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 )
103 82 102 jca ⊢ ( ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) )
104 51 103 mpancom ⊢ ( ( ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) )
105 104 exp31 ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) ) )
106 105 com23 ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) → ( ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) ) )
107 106 ancoms ⊢ ( ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ) → ( ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) ) )
108 50 107 syl ⊢ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) → ( ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) ) )
109 108 imp ⊢ ( ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) )
110 109 com12 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) )
111 110 3adant1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) )
112 111 imp ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) )
113 49 112 jca ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) )
114 113 ex ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) ) )
115 21 114 sylbid ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) ) )
116 115 imp ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) )
117 3simpc ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) )
118 117 adantr ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) )
119 1 2 numclwwlkovq ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 𝑄 𝑁 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } )
120 118 119 syl ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( 𝑋 𝑄 𝑁 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } )
121 120 eleq2d ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑋 𝑄 𝑁 ) ↔ ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) )
122 fveq1 ⊢ ( 𝑤 = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( 𝑤 ‘ 0 ) = ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) )
123 122 eqeq1d ⊢ ( 𝑤 = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( ( 𝑤 ‘ 0 ) = 𝑋 ↔ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ) )
124 fveq2 ⊢ ( 𝑤 = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( lastS ‘ 𝑤 ) = ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) )
125 124 neeq1d ⊢ ( 𝑤 = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( ( lastS ‘ 𝑤 ) ≠ 𝑋 ↔ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) )
126 123 125 anbi12d ⊢ ( 𝑤 = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) ↔ ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) )
127 126 elrab ⊢ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ↔ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) )
128 121 127 bitrdi ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑋 𝑄 𝑁 ) ↔ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑋 ∧ ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ≠ 𝑋 ) ) ) )
129 116 128 mpbird ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑋 𝑄 𝑁 ) )
130 129 4 fmptd ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑅 : ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ⟶ ( 𝑋 𝑄 𝑁 ) )