Metamath Proof Explorer


Theorem extwwlkfab

Description: The set ( X C N ) of double loops of length N on vertex X can be constructed from the set F of closed walks on X with length smaller by 2 than the fixed length by appending a neighbor of the last vertex and afterwards the last vertex (which is the first vertex) itself ("walking forth and back" from the last vertex). 3 <_ N is required since for N = 2 : F = ( X ( ClWWalksNOnG ) 0 ) = (/) (see clwwlk0on0 stating that a closed walk of length 0 is not represented as word), which would result in an empty set on the right hand side, but ( X C N ) needs not be empty, see 2clwwlk2 . (Contributed by Alexander van der Vekens, 18-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 31-Oct-2022)

Ref Expression
Hypotheses extwwlkfab.v 𝑉 = ( Vtx ‘ 𝐺 )
extwwlkfab.c 𝐶 = ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
extwwlkfab.f 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
Assertion extwwlkfab ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } )

Proof

Step Hyp Ref Expression
1 extwwlkfab.v 𝑉 = ( Vtx ‘ 𝐺 )
2 extwwlkfab.c 𝐶 = ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
3 extwwlkfab.f 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
4 uzuzle23 ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 ∈ ( ℤ ‘ 2 ) )
5 2 2clwwlk ( ( 𝑋𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
6 4 5 sylan2 ( ( 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
7 6 3adant1 ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
8 clwwlknon ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 }
9 8 rabeqi { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } = { 𝑤 ∈ { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 }
10 rabrab { 𝑤 ∈ { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
11 simpll3 ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → 𝑁 ∈ ( ℤ ‘ 3 ) )
12 simplr ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) )
13 simpr ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 )
14 simpl ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑤 ‘ 0 ) = 𝑋 )
15 14 eqcomd ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → 𝑋 = ( 𝑤 ‘ 0 ) )
16 13 15 eqtrd ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑤 ‘ ( 𝑁 − 2 ) ) = ( 𝑤 ‘ 0 ) )
17 16 adantl ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑤 ‘ ( 𝑁 − 2 ) ) = ( 𝑤 ‘ 0 ) )
18 clwwnrepclwwn ( ( 𝑁 ∈ ( ℤ ‘ 3 ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = ( 𝑤 ‘ 0 ) ) → ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) )
19 11 12 17 18 syl3anc ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) )
20 14 adantl ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑤 ‘ 0 ) = 𝑋 )
21 19 20 jca ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
22 simp1 ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → 𝐺 ∈ USGraph )
23 22 anim1i ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( 𝐺 ∈ USGraph ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) )
24 23 adantr ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝐺 ∈ USGraph ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) )
25 clwwlknlbonbgr1 ( ( 𝐺 ∈ USGraph ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx ( 𝑤 ‘ 0 ) ) )
26 24 25 syl ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx ( 𝑤 ‘ 0 ) ) )
27 oveq2 ( 𝑋 = ( 𝑤 ‘ 0 ) → ( 𝐺 NeighbVtx 𝑋 ) = ( 𝐺 NeighbVtx ( 𝑤 ‘ 0 ) ) )
28 27 eqcoms ( ( 𝑤 ‘ 0 ) = 𝑋 → ( 𝐺 NeighbVtx 𝑋 ) = ( 𝐺 NeighbVtx ( 𝑤 ‘ 0 ) ) )
29 28 adantr ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝐺 NeighbVtx 𝑋 ) = ( 𝐺 NeighbVtx ( 𝑤 ‘ 0 ) ) )
30 29 adantl ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝐺 NeighbVtx 𝑋 ) = ( 𝐺 NeighbVtx ( 𝑤 ‘ 0 ) ) )
31 26 30 eleqtrrd ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) )
32 13 adantl ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 )
33 21 31 32 3jca ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
34 33 ex ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
35 simpr ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) → ( 𝑤 ‘ 0 ) = 𝑋 )
36 35 anim1i ( ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
37 36 3adant2 ( ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
38 34 37 impbid1 ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
39 2clwwlklem ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = ( 𝑤 ‘ 0 ) )
40 39 3ad2antr3 ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = ( 𝑤 ‘ 0 ) )
41 40 ancoms ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = ( 𝑤 ‘ 0 ) )
42 41 eqcomd ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( 𝑤 ‘ 0 ) = ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ‘ 0 ) )
43 42 eqeq1d ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ( 𝑤 ‘ 0 ) = 𝑋 ↔ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = 𝑋 ) )
44 43 anbi2d ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = 𝑋 ) ) )
45 44 3anbi1d ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
46 3 eleq2i ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ↔ ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) )
47 isclwwlknon ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ↔ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = 𝑋 ) )
48 47 a1i ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ↔ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = 𝑋 ) ) )
49 46 48 syl5bb ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ↔ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = 𝑋 ) ) )
50 49 3anbi1d ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
51 50 bicomd ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
52 51 adantr ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ‘ 0 ) = 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
53 38 45 52 3bitrd ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ∧ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
54 53 rabbidva ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } )
55 10 54 syl5eq ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → { 𝑤 ∈ { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } )
56 9 55 syl5eq ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } )
57 7 56 eqtrd ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } )