Metamath Proof Explorer

Theorem numclwwlk2lem1

Description: In a friendship graph, for each walk of length n starting at a fixed vertex v and ending not at this vertex, there is a unique vertex so that the walk extended by an edge to this vertex and an edge from this vertex to the first vertex of the walk is a value of operation H . If the walk is represented as a word, it is sufficient to add one vertex to the word to obtain the closed walk contained in the value of operation H , since in a word representing a closed walk the starting vertex is not repeated at the end. This theorem generally holds only for friendship graphs, because these guarantee that for the first and last vertex there is a (unique) third vertex "in between". (Contributed by Alexander van der Vekens, 3-Oct-2018) (Revised by AV, 30-May-2021) (Revised by AV, 1-May-2022)

Ref Expression
Hypotheses numclwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
numclwwlk.q ⊢ 𝑄 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
numclwwlk.h ⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
Assertion numclwwlk2lem1 ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ ( 𝑋 𝑄 𝑁 ) → ∃! 𝑣 ∈ 𝑉 ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 numclwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 numclwwlk.q ⊢ 𝑄 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
3 numclwwlk.h ⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
4 1 2 numclwwlkovq ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 𝑄 𝑁 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } )
5 4 3adant1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 𝑄 𝑁 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } )
6 5 eleq2d ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ ( 𝑋 𝑄 𝑁 ) ↔ 𝑊 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) )
7 fveq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ 0 ) = ( 𝑊 ‘ 0 ) )
8 7 eqeq1d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ‘ 0 ) = 𝑋 ↔ ( 𝑊 ‘ 0 ) = 𝑋 ) )
9 fveq2 ⊢ ( 𝑤 = 𝑊 → ( lastS ‘ 𝑤 ) = ( lastS ‘ 𝑊 ) )
10 9 neeq1d ⊢ ( 𝑤 = 𝑊 → ( ( lastS ‘ 𝑤 ) ≠ 𝑋 ↔ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) )
11 8 10 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) ↔ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) )
12 11 elrab ⊢ ( 𝑊 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) )
13 6 12 bitrdi ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ ( 𝑋 𝑄 𝑁 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) )
14 simpl1 ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) → 𝐺 ∈ FriendGraph )
15 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
16 1 15 wwlknp ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
17 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
18 17 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 + 1 ) ∈ ℕ )
19 simpl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) )
20 18 19 jca ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) )
21 20 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ) )
22 21 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ) )
23 16 22 syl ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ) )
24 lswlgt0cl ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( lastS ‘ 𝑊 ) ∈ 𝑉 )
25 23 24 syl6 ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ → ( lastS ‘ 𝑊 ) ∈ 𝑉 ) )
26 25 adantr ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) → ( 𝑁 ∈ ℕ → ( lastS ‘ 𝑊 ) ∈ 𝑉 ) )
27 26 com12 ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) → ( lastS ‘ 𝑊 ) ∈ 𝑉 ) )
28 27 3ad2ant3 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) → ( lastS ‘ 𝑊 ) ∈ 𝑉 ) )
29 28 imp ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) → ( lastS ‘ 𝑊 ) ∈ 𝑉 )
30 eleq1 ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → ( ( 𝑊 ‘ 0 ) ∈ 𝑉 ↔ 𝑋 ∈ 𝑉 ) )
31 30 biimprd ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → ( 𝑋 ∈ 𝑉 → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) )
32 31 ad2antrl ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) → ( 𝑋 ∈ 𝑉 → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) )
33 32 com12 ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) )
34 33 3ad2ant2 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) )
35 34 imp ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
36 neeq2 ⊢ ( 𝑋 = ( 𝑊 ‘ 0 ) → ( ( lastS ‘ 𝑊 ) ≠ 𝑋 ↔ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) )
37 36 eqcoms ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → ( ( lastS ‘ 𝑊 ) ≠ 𝑋 ↔ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) )
38 37 biimpa ⊢ ( ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) → ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) )
39 38 adantl ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) → ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) )
40 39 adantl ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) → ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) )
41 29 35 40 3jca ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) → ( ( lastS ‘ 𝑊 ) ∈ 𝑉 ∧ ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) )
42 1 15 frcond2 ⊢ ( 𝐺 ∈ FriendGraph → ( ( ( lastS ‘ 𝑊 ) ∈ 𝑉 ∧ ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) → ∃! 𝑣 ∈ 𝑉 ( { ( lastS ‘ 𝑊 ) , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑣 , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
43 14 41 42 sylc ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) → ∃! 𝑣 ∈ 𝑉 ( { ( lastS ‘ 𝑊 ) , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑣 , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
44 simpl ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) )
45 44 ad2antlr ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) )
46 simpr ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
47 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
48 47 3ad2ant3 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
49 48 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑁 ∈ ℕ0 )
50 45 46 49 3jca ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑣 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) )
51 1 15 wwlksext2clwwlk ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( { ( lastS ‘ 𝑊 ) , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑣 , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) )
52 51 3adant3 ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑣 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( { ( lastS ‘ 𝑊 ) , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑣 , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) )
53 52 imp ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ 𝑣 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑣 , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) )
54 50 53 sylan ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( { ( lastS ‘ 𝑊 ) , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑣 , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) )
55 1 wwlknbp ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) )
56 55 simp3d ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝑊 ∈ Word 𝑉 )
57 56 ad2antrl ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) → 𝑊 ∈ Word 𝑉 )
58 57 ad2antrr ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) → 𝑊 ∈ Word 𝑉 )
59 46 adantr ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) → 𝑣 ∈ 𝑉 )
60 2z ⊢ 2 ∈ ℤ
61 nn0pzuz ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ∈ ℤ ) → ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) )
62 47 60 61 sylancl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) )
63 62 3ad2ant3 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) )
64 63 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) → ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) )
65 simpr ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) → ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) )
66 1 15 clwwlkext2edg ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑣 , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
67 58 59 64 65 66 syl31anc ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑣 , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
68 54 67 impbida ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( { ( lastS ‘ 𝑊 ) , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑣 , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ) )
69 46 1 eleqtrdi ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ ( Vtx ‘ 𝐺 ) )
70 38 anim2i ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) )
71 70 ad2antlr ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) )
72 71 simprd ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) )
73 numclwwlk2lem1lem ⊢ ( ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 𝑁 ) ≠ ( 𝑊 ‘ 0 ) ) )
74 69 45 72 73 syl3anc ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 𝑁 ) ≠ ( 𝑊 ‘ 0 ) ) )
75 eqeq2 ⊢ ( 𝑋 = ( 𝑊 ‘ 0 ) → ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ↔ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) )
76 75 eqcoms ⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ↔ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) )
77 76 ad2antrl ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ↔ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) )
78 77 ad2antlr ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ↔ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) )
79 74 simpld ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
80 79 neeq2d ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 𝑁 ) ≠ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) ↔ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 𝑁 ) ≠ ( 𝑊 ‘ 0 ) ) )
81 78 80 anbi12d ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 𝑁 ) ≠ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 𝑁 ) ≠ ( 𝑊 ‘ 0 ) ) ) )
82 74 81 mpbird ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 𝑁 ) ≠ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) ) )
83 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
84 2cnd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
85 83 84 pncand ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 2 ) − 2 ) = 𝑁 )
86 85 3ad2ant3 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 + 2 ) − 2 ) = 𝑁 )
87 86 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑁 + 2 ) − 2 ) = 𝑁 )
88 87 fveq2d ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ ( ( 𝑁 + 2 ) − 2 ) ) = ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 𝑁 ) )
89 88 neeq1d ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) ↔ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 𝑁 ) ≠ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) ) )
90 89 anbi2d ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 𝑁 ) ≠ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) ) ) )
91 82 90 mpbird ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) ) )
92 91 biantrud ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ↔ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) ) ) ) )
93 62 anim2i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) ) )
94 93 3adant1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) ) )
95 94 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) ) )
96 3 numclwwlkovh ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐻 ( 𝑁 + 2 ) ) = { 𝑤 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } )
97 95 96 syl ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑋 𝐻 ( 𝑁 + 2 ) ) = { 𝑤 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } )
98 97 eleq2d ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↔ ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ { 𝑤 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } ) )
99 fveq1 ⊢ ( 𝑤 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) → ( 𝑤 ‘ 0 ) = ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) )
100 99 eqeq1d ⊢ ( 𝑤 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) → ( ( 𝑤 ‘ 0 ) = 𝑋 ↔ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ) )
101 fveq1 ⊢ ( 𝑤 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) → ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) = ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ ( ( 𝑁 + 2 ) − 2 ) ) )
102 101 99 neeq12d ⊢ ( 𝑤 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) → ( ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ↔ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) ) )
103 100 102 anbi12d ⊢ ( 𝑤 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) ) ) )
104 103 elrab ⊢ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ { 𝑤 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } ↔ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) ) ) )
105 98 104 bitr2di ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) = 𝑋 ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ‘ 0 ) ) ) ↔ ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) )
106 68 92 105 3bitrd ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( { ( lastS ‘ 𝑊 ) , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑣 , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) )
107 106 reubidva ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) → ( ∃! 𝑣 ∈ 𝑉 ( { ( lastS ‘ 𝑊 ) , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑣 , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ∃! 𝑣 ∈ 𝑉 ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) )
108 43 107 mpbid ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) ) → ∃! 𝑣 ∈ 𝑉 ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) )
109 108 ex ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑊 ) ≠ 𝑋 ) ) → ∃! 𝑣 ∈ 𝑉 ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) )
110 13 109 sylbid ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ ( 𝑋 𝑄 𝑁 ) → ∃! 𝑣 ∈ 𝑉 ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) )