Metamath Proof Explorer

Theorem numclwwlk1lem2foa

Description: Going forth and back from the end of a (closed) walk: W represents the closed walk p_0, ..., p_(n-2), p_0 = p_(n-2). With X = p_(n-2) = p_0 and Y = p_(n-1), ( ( W ++ <" X "> ) ++ <" Y "> ) represents the closed walk p_0, ..., p_(n-2), p_(n-1), p_n = p_0 which is a double loop of length N on vertex X . (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 5-Mar-2022) (Proof shortened by AV, 2-Nov-2022)

Ref Expression
Hypotheses extwwlkfab.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
extwwlkfab.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
extwwlkfab.f ⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
Assertion numclwwlk1lem2foa ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 extwwlkfab.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 extwwlkfab.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
3 extwwlkfab.f ⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
4 simpl2 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → 𝑋 ∈ 𝑉 )
5 1 nbgrisvtx ⊢ ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑌 ∈ 𝑉 )
6 5 ad2antll ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → 𝑌 ∈ 𝑉 )
7 simpl3 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
8 nbgrsym ⊢ ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ 𝑋 ∈ ( 𝐺 NeighbVtx 𝑌 ) )
9 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
10 9 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑋 ∈ ( 𝐺 NeighbVtx 𝑌 ) ↔ { 𝑋 , 𝑌 } ∈ ( Edg ‘ 𝐺 ) ) )
11 10 biimpd ⊢ ( 𝐺 ∈ USGraph → ( 𝑋 ∈ ( 𝐺 NeighbVtx 𝑌 ) → { 𝑋 , 𝑌 } ∈ ( Edg ‘ 𝐺 ) ) )
12 8 11 syl5bi ⊢ ( 𝐺 ∈ USGraph → ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) → { 𝑋 , 𝑌 } ∈ ( Edg ‘ 𝐺 ) ) )
13 12 adantld ⊢ ( 𝐺 ∈ USGraph → ( ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) → { 𝑋 , 𝑌 } ∈ ( Edg ‘ 𝐺 ) ) )
14 13 3ad2ant1 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) → { 𝑋 , 𝑌 } ∈ ( Edg ‘ 𝐺 ) ) )
15 14 imp ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → { 𝑋 , 𝑌 } ∈ ( Edg ‘ 𝐺 ) )
16 simprl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → 𝑊 ∈ 𝐹 )
17 16 3 eleqtrdi ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) )
18 1 9 clwwlknonex2 ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ ( Edg ‘ 𝐺 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )
19 4 6 7 15 17 18 syl311anc ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )
20 3 eleq2i ⊢ ( 𝑊 ∈ 𝐹 ↔ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) )
21 uz3m2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℕ )
22 21 nnne0d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ≠ 0 )
23 1 9 clwwlknonel ⊢ ( ( 𝑁 − 2 ) ≠ 0 → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
24 22 23 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
25 24 3ad2ant3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
26 20 25 syl5bb ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ 𝐹 ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) )
27 3simpa ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) )
28 27 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) )
29 simp32 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝑋 ∈ 𝑉 )
30 29 5 anim12i ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) )
31 simpl33 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
32 28 30 31 3jca ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) )
33 32 3exp1 ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) ) )
34 33 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) ) )
35 34 imp ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) )
36 35 3adant3 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) )
37 36 com12 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) )
38 26 37 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ 𝐹 → ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) )
39 38 imp32 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) )
40 numclwwlk1lem2foalem ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) = 𝑊 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) = 𝑌 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
41 39 40 syl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) = 𝑊 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) = 𝑌 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
42 eleq1a ⊢ ( 𝑊 ∈ 𝐹 → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) = 𝑊 → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ) )
43 16 42 syl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) = 𝑊 → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ) )
44 eleq1a ⊢ ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) = 𝑌 → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ) )
45 44 ad2antll ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) = 𝑌 → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ) )
46 idd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
47 43 45 46 3anim123d ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) = 𝑊 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) = 𝑌 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
48 41 47 mpd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
49 1 2 3 extwwlkfabel ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )
50 49 adantr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )
51 19 48 50 mpbir2and ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) )
52 51 ex ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑊 ∈ 𝐹 ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ) )