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 
|- V = ( Vtx ` G )
numclwwlk.q 
|- Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
numclwwlk.h 
|- H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
Assertion numclwwlk2lem1 
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( W e. ( X Q N ) -> E! v e. V ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 numclwwlk.v 
 |-  V = ( Vtx ` G )
2 numclwwlk.q 
 |-  Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
3 numclwwlk.h 
 |-  H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
4 1 2 numclwwlkovq 
 |-  ( ( X e. V /\ N e. NN ) -> ( X Q N ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } )
5 4 3adant1 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( X Q N ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } )
6 5 eleq2d 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( W e. ( X Q N ) <-> W e. { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } ) )
7 fveq1 
 |-  ( w = W -> ( w ` 0 ) = ( W ` 0 ) )
8 7 eqeq1d 
 |-  ( w = W -> ( ( w ` 0 ) = X <-> ( W ` 0 ) = X ) )
9 fveq2 
 |-  ( w = W -> ( lastS ` w ) = ( lastS ` W ) )
10 9 neeq1d 
 |-  ( w = W -> ( ( lastS ` w ) =/= X <-> ( lastS ` W ) =/= X ) )
11 8 10 anbi12d 
 |-  ( w = W -> ( ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) <-> ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) )
12 11 elrab 
 |-  ( W e. { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } <-> ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) )
13 6 12 bitrdi 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( W e. ( X Q N ) <-> ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) )
14 simpl1 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> G e. FriendGraph )
15 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
16 1 15 wwlknp 
 |-  ( W e. ( N WWalksN G ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
17 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
18 17 adantl 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ N e. NN ) -> ( N + 1 ) e. NN )
19 simpl 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ N e. NN ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) )
20 18 19 jca 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ N e. NN ) -> ( ( N + 1 ) e. NN /\ ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) ) )
21 20 ex 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( N e. NN -> ( ( N + 1 ) e. NN /\ ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) ) ) )
22 21 3adant3 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( N e. NN -> ( ( N + 1 ) e. NN /\ ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) ) ) )
23 16 22 syl 
 |-  ( W e. ( N WWalksN G ) -> ( N e. NN -> ( ( N + 1 ) e. NN /\ ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) ) ) )
24 lswlgt0cl 
 |-  ( ( ( N + 1 ) e. NN /\ ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) ) -> ( lastS ` W ) e. V )
25 23 24 syl6 
 |-  ( W e. ( N WWalksN G ) -> ( N e. NN -> ( lastS ` W ) e. V ) )
26 25 adantr 
 |-  ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( N e. NN -> ( lastS ` W ) e. V ) )
27 26 com12 
 |-  ( N e. NN -> ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( lastS ` W ) e. V ) )
28 27 3ad2ant3 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( lastS ` W ) e. V ) )
29 28 imp 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> ( lastS ` W ) e. V )
30 eleq1 
 |-  ( ( W ` 0 ) = X -> ( ( W ` 0 ) e. V <-> X e. V ) )
31 30 biimprd 
 |-  ( ( W ` 0 ) = X -> ( X e. V -> ( W ` 0 ) e. V ) )
32 31 ad2antrl 
 |-  ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( X e. V -> ( W ` 0 ) e. V ) )
33 32 com12 
 |-  ( X e. V -> ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( W ` 0 ) e. V ) )
34 33 3ad2ant2 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( W ` 0 ) e. V ) )
35 34 imp 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> ( W ` 0 ) e. V )
36 neeq2 
 |-  ( X = ( W ` 0 ) -> ( ( lastS ` W ) =/= X <-> ( lastS ` W ) =/= ( W ` 0 ) ) )
37 36 eqcoms 
 |-  ( ( W ` 0 ) = X -> ( ( lastS ` W ) =/= X <-> ( lastS ` W ) =/= ( W ` 0 ) ) )
38 37 biimpa 
 |-  ( ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) -> ( lastS ` W ) =/= ( W ` 0 ) )
39 38 adantl 
 |-  ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( lastS ` W ) =/= ( W ` 0 ) )
40 39 adantl 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> ( lastS ` W ) =/= ( W ` 0 ) )
41 29 35 40 3jca 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> ( ( lastS ` W ) e. V /\ ( W ` 0 ) e. V /\ ( lastS ` W ) =/= ( W ` 0 ) ) )
42 1 15 frcond2 
 |-  ( G e. FriendGraph -> ( ( ( lastS ` W ) e. V /\ ( W ` 0 ) e. V /\ ( lastS ` W ) =/= ( W ` 0 ) ) -> E! v e. V ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
43 14 41 42 sylc 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> E! v e. V ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) )
44 simpl 
 |-  ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> W e. ( N WWalksN G ) )
45 44 ad2antlr 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> W e. ( N WWalksN G ) )
46 simpr 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> v e. V )
47 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
48 47 3ad2ant3 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> N e. NN0 )
49 48 ad2antrr 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> N e. NN0 )
50 45 46 49 3jca 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( W e. ( N WWalksN G ) /\ v e. V /\ N e. NN0 ) )
51 1 15 wwlksext2clwwlk 
 |-  ( ( W e. ( N WWalksN G ) /\ v e. V ) -> ( ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) )
52 51 3adant3 
 |-  ( ( W e. ( N WWalksN G ) /\ v e. V /\ N e. NN0 ) -> ( ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) )
53 52 imp 
 |-  ( ( ( W e. ( N WWalksN G ) /\ v e. V /\ N e. NN0 ) /\ ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) ) -> ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) )
54 50 53 sylan 
 |-  ( ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) /\ ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) ) -> ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) )
55 1 wwlknbp 
 |-  ( W e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ W e. Word V ) )
56 55 simp3d 
 |-  ( W e. ( N WWalksN G ) -> W e. Word V )
57 56 ad2antrl 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> W e. Word V )
58 57 ad2antrr 
 |-  ( ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) /\ ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) -> W e. Word V )
59 46 adantr 
 |-  ( ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) /\ ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) -> v e. V )
60 2z 
 |-  2 e. ZZ
61 nn0pzuz 
 |-  ( ( N e. NN0 /\ 2 e. ZZ ) -> ( N + 2 ) e. ( ZZ>= ` 2 ) )
62 47 60 61 sylancl 
 |-  ( N e. NN -> ( N + 2 ) e. ( ZZ>= ` 2 ) )
63 62 3ad2ant3 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( N + 2 ) e. ( ZZ>= ` 2 ) )
64 63 ad3antrrr 
 |-  ( ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) /\ ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) -> ( N + 2 ) e. ( ZZ>= ` 2 ) )
65 simpr 
 |-  ( ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) /\ ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) -> ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) )
66 1 15 clwwlkext2edg 
 |-  ( ( ( W e. Word V /\ v e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) /\ ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) -> ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) )
67 58 59 64 65 66 syl31anc 
 |-  ( ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) /\ ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) -> ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) )
68 54 67 impbida 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) )
69 46 1 eleqtrdi 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> v e. ( Vtx ` G ) )
70 38 anim2i 
 |-  ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( W e. ( N WWalksN G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) )
71 70 ad2antlr 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( W e. ( N WWalksN G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) )
72 71 simprd 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( lastS ` W ) =/= ( W ` 0 ) )
73 numclwwlk2lem1lem 
 |-  ( ( v e. ( Vtx ` G ) /\ W e. ( N WWalksN G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) -> ( ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) /\ ( ( W ++ <" v "> ) ` N ) =/= ( W ` 0 ) ) )
74 69 45 72 73 syl3anc 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) /\ ( ( W ++ <" v "> ) ` N ) =/= ( W ` 0 ) ) )
75 eqeq2 
 |-  ( X = ( W ` 0 ) -> ( ( ( W ++ <" v "> ) ` 0 ) = X <-> ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) ) )
76 75 eqcoms 
 |-  ( ( W ` 0 ) = X -> ( ( ( W ++ <" v "> ) ` 0 ) = X <-> ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) ) )
77 76 ad2antrl 
 |-  ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( ( ( W ++ <" v "> ) ` 0 ) = X <-> ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) ) )
78 77 ad2antlr 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) ` 0 ) = X <-> ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) ) )
79 74 simpld 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) )
80 79 neeq2d 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) ` N ) =/= ( ( W ++ <" v "> ) ` 0 ) <-> ( ( W ++ <" v "> ) ` N ) =/= ( W ` 0 ) ) )
81 78 80 anbi12d 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` N ) =/= ( ( W ++ <" v "> ) ` 0 ) ) <-> ( ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) /\ ( ( W ++ <" v "> ) ` N ) =/= ( W ` 0 ) ) ) )
82 74 81 mpbird 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` N ) =/= ( ( W ++ <" v "> ) ` 0 ) ) )
83 nncn 
 |-  ( N e. NN -> N e. CC )
84 2cnd 
 |-  ( N e. NN -> 2 e. CC )
85 83 84 pncand 
 |-  ( N e. NN -> ( ( N + 2 ) - 2 ) = N )
86 85 3ad2ant3 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( N + 2 ) - 2 ) = N )
87 86 ad2antrr 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( N + 2 ) - 2 ) = N )
88 87 fveq2d 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) = ( ( W ++ <" v "> ) ` N ) )
89 88 neeq1d 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) <-> ( ( W ++ <" v "> ) ` N ) =/= ( ( W ++ <" v "> ) ` 0 ) ) )
90 89 anbi2d 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) <-> ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` N ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) )
91 82 90 mpbird 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) )
92 91 biantrud 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) <-> ( ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) ) )
93 62 anim2i 
 |-  ( ( X e. V /\ N e. NN ) -> ( X e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) )
94 93 3adant1 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( X e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) )
95 94 ad2antrr 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( X e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) )
96 3 numclwwlkovh 
 |-  ( ( X e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) -> ( X H ( N + 2 ) ) = { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } )
97 95 96 syl 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( X H ( N + 2 ) ) = { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } )
98 97 eleq2d 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) <-> ( W ++ <" v "> ) e. { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } ) )
99 fveq1 
 |-  ( w = ( W ++ <" v "> ) -> ( w ` 0 ) = ( ( W ++ <" v "> ) ` 0 ) )
100 99 eqeq1d 
 |-  ( w = ( W ++ <" v "> ) -> ( ( w ` 0 ) = X <-> ( ( W ++ <" v "> ) ` 0 ) = X ) )
101 fveq1 
 |-  ( w = ( W ++ <" v "> ) -> ( w ` ( ( N + 2 ) - 2 ) ) = ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) )
102 101 99 neeq12d 
 |-  ( w = ( W ++ <" v "> ) -> ( ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) <-> ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) )
103 100 102 anbi12d 
 |-  ( w = ( W ++ <" v "> ) -> ( ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) <-> ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) )
104 103 elrab 
 |-  ( ( W ++ <" v "> ) e. { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } <-> ( ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) )
105 98 104 bitr2di 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) <-> ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) ) )
106 68 92 105 3bitrd 
 |-  ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) ) )
107 106 reubidva 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> ( E! v e. V ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) <-> E! v e. V ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) ) )
108 43 107 mpbid 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> E! v e. V ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) )
109 108 ex 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> E! v e. V ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) ) )
110 13 109 sylbid 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( W e. ( X Q N ) -> E! v e. V ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) ) )