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 bitrid ⊢ ( ( 𝐺 ∈ 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 eqtrid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → { 𝑤 ∈ { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } )
56 9 55 eqtrid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } )
57 7 56 eqtrd ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } )