Metamath Proof Explorer

Theorem numclwlk2lem2f

Description: R is a function mapping the "closed (n+2)-walks v(0) ... v(n-2) v(n-1) v(n) v(n+1) v(n+2) starting at X = v(0) = v(n+2) with v(n) =/= X" to the words representing the prefix v(0) ... v(n-2) v(n-1) v(n) of the walk. (Contributed by Alexander van der Vekens, 5-Oct-2018) (Revised by AV, 31-May-2021) (Proof shortened by AV, 23-Mar-2022) (Revised by AV, 1-Nov-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 } )
numclwwlk.r 
|- R = ( x e. ( X H ( N + 2 ) ) |-> ( x prefix ( N + 1 ) ) )
Assertion numclwlk2lem2f 
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> R : ( X H ( N + 2 ) ) --> ( X Q N ) )

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 numclwwlk.r 
 |-  R = ( x e. ( X H ( N + 2 ) ) |-> ( x prefix ( N + 1 ) ) )
5 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
6 2z 
 |-  2 e. ZZ
7 6 a1i 
 |-  ( N e. NN -> 2 e. ZZ )
8 nn0pzuz 
 |-  ( ( N e. NN0 /\ 2 e. ZZ ) -> ( N + 2 ) e. ( ZZ>= ` 2 ) )
9 5 7 8 syl2anc 
 |-  ( N e. NN -> ( N + 2 ) e. ( ZZ>= ` 2 ) )
10 9 anim2i 
 |-  ( ( X e. V /\ N e. NN ) -> ( X e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) )
11 10 3adant1 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( X e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) )
12 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 ) ) } )
13 12 eleq2d 
 |-  ( ( X e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) -> ( x e. ( X H ( N + 2 ) ) <-> x e. { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } ) )
14 11 13 syl 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( x e. ( X H ( N + 2 ) ) <-> x e. { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } ) )
15 fveq1 
 |-  ( w = x -> ( w ` 0 ) = ( x ` 0 ) )
16 15 eqeq1d 
 |-  ( w = x -> ( ( w ` 0 ) = X <-> ( x ` 0 ) = X ) )
17 fveq1 
 |-  ( w = x -> ( w ` ( ( N + 2 ) - 2 ) ) = ( x ` ( ( N + 2 ) - 2 ) ) )
18 17 15 neeq12d 
 |-  ( w = x -> ( ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) <-> ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) )
19 16 18 anbi12d 
 |-  ( w = x -> ( ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) <-> ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) )
20 19 elrab 
 |-  ( x e. { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } <-> ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) )
21 14 20 bitrdi 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( x e. ( X H ( N + 2 ) ) <-> ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) )
22 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
23 nnz 
 |-  ( N e. NN -> N e. ZZ )
24 23 7 zaddcld 
 |-  ( N e. NN -> ( N + 2 ) e. ZZ )
25 uzid 
 |-  ( ( N + 2 ) e. ZZ -> ( N + 2 ) e. ( ZZ>= ` ( N + 2 ) ) )
26 24 25 syl 
 |-  ( N e. NN -> ( N + 2 ) e. ( ZZ>= ` ( N + 2 ) ) )
27 nncn 
 |-  ( N e. NN -> N e. CC )
28 1cnd 
 |-  ( N e. NN -> 1 e. CC )
29 27 28 28 addassd 
 |-  ( N e. NN -> ( ( N + 1 ) + 1 ) = ( N + ( 1 + 1 ) ) )
30 1p1e2 
 |-  ( 1 + 1 ) = 2
31 30 a1i 
 |-  ( N e. NN -> ( 1 + 1 ) = 2 )
32 31 oveq2d 
 |-  ( N e. NN -> ( N + ( 1 + 1 ) ) = ( N + 2 ) )
33 29 32 eqtrd 
 |-  ( N e. NN -> ( ( N + 1 ) + 1 ) = ( N + 2 ) )
34 33 fveq2d 
 |-  ( N e. NN -> ( ZZ>= ` ( ( N + 1 ) + 1 ) ) = ( ZZ>= ` ( N + 2 ) ) )
35 26 34 eleqtrrd 
 |-  ( N e. NN -> ( N + 2 ) e. ( ZZ>= ` ( ( N + 1 ) + 1 ) ) )
36 22 35 jca 
 |-  ( N e. NN -> ( ( N + 1 ) e. NN /\ ( N + 2 ) e. ( ZZ>= ` ( ( N + 1 ) + 1 ) ) ) )
37 36 3ad2ant3 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( N + 1 ) e. NN /\ ( N + 2 ) e. ( ZZ>= ` ( ( N + 1 ) + 1 ) ) ) )
38 37 adantr 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( N + 1 ) e. NN /\ ( N + 2 ) e. ( ZZ>= ` ( ( N + 1 ) + 1 ) ) ) )
39 simprl 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> x e. ( ( N + 2 ) ClWWalksN G ) )
40 wwlksubclwwlk 
 |-  ( ( ( N + 1 ) e. NN /\ ( N + 2 ) e. ( ZZ>= ` ( ( N + 1 ) + 1 ) ) ) -> ( x e. ( ( N + 2 ) ClWWalksN G ) -> ( x prefix ( N + 1 ) ) e. ( ( ( N + 1 ) - 1 ) WWalksN G ) ) )
41 38 39 40 sylc 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( x prefix ( N + 1 ) ) e. ( ( ( N + 1 ) - 1 ) WWalksN G ) )
42 pncan1 
 |-  ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
43 42 eqcomd 
 |-  ( N e. CC -> N = ( ( N + 1 ) - 1 ) )
44 27 43 syl 
 |-  ( N e. NN -> N = ( ( N + 1 ) - 1 ) )
45 44 oveq1d 
 |-  ( N e. NN -> ( N WWalksN G ) = ( ( ( N + 1 ) - 1 ) WWalksN G ) )
46 45 eleq2d 
 |-  ( N e. NN -> ( ( x prefix ( N + 1 ) ) e. ( N WWalksN G ) <-> ( x prefix ( N + 1 ) ) e. ( ( ( N + 1 ) - 1 ) WWalksN G ) ) )
47 46 3ad2ant3 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( x prefix ( N + 1 ) ) e. ( N WWalksN G ) <-> ( x prefix ( N + 1 ) ) e. ( ( ( N + 1 ) - 1 ) WWalksN G ) ) )
48 47 adantr 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( x prefix ( N + 1 ) ) e. ( N WWalksN G ) <-> ( x prefix ( N + 1 ) ) e. ( ( ( N + 1 ) - 1 ) WWalksN G ) ) )
49 41 48 mpbird 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( x prefix ( N + 1 ) ) e. ( N WWalksN G ) )
50 1 clwwlknbp 
 |-  ( x e. ( ( N + 2 ) ClWWalksN G ) -> ( x e. Word V /\ ( # ` x ) = ( N + 2 ) ) )
51 simprl 
 |-  ( ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( x ` 0 ) = X )
52 simprr 
 |-  ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> x e. Word V )
53 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
54 5 53 syl 
 |-  ( N e. NN -> ( N + 1 ) e. NN0 )
55 nnre 
 |-  ( N e. NN -> N e. RR )
56 55 lep1d 
 |-  ( N e. NN -> N <_ ( N + 1 ) )
57 elfz2nn0 
 |-  ( N e. ( 0 ... ( N + 1 ) ) <-> ( N e. NN0 /\ ( N + 1 ) e. NN0 /\ N <_ ( N + 1 ) ) )
58 5 54 56 57 syl3anbrc 
 |-  ( N e. NN -> N e. ( 0 ... ( N + 1 ) ) )
59 2cnd 
 |-  ( N e. NN -> 2 e. CC )
60 addsubass 
 |-  ( ( N e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( N + 2 ) - 1 ) = ( N + ( 2 - 1 ) ) )
61 2m1e1 
 |-  ( 2 - 1 ) = 1
62 61 oveq2i 
 |-  ( N + ( 2 - 1 ) ) = ( N + 1 )
63 60 62 eqtrdi 
 |-  ( ( N e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( N + 2 ) - 1 ) = ( N + 1 ) )
64 27 59 28 63 syl3anc 
 |-  ( N e. NN -> ( ( N + 2 ) - 1 ) = ( N + 1 ) )
65 64 oveq2d 
 |-  ( N e. NN -> ( 0 ... ( ( N + 2 ) - 1 ) ) = ( 0 ... ( N + 1 ) ) )
66 58 65 eleqtrrd 
 |-  ( N e. NN -> N e. ( 0 ... ( ( N + 2 ) - 1 ) ) )
67 elfzp1b 
 |-  ( ( N e. ZZ /\ ( N + 2 ) e. ZZ ) -> ( N e. ( 0 ... ( ( N + 2 ) - 1 ) ) <-> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) ) )
68 23 24 67 syl2anc 
 |-  ( N e. NN -> ( N e. ( 0 ... ( ( N + 2 ) - 1 ) ) <-> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) ) )
69 66 68 mpbid 
 |-  ( N e. NN -> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) )
70 69 adantr 
 |-  ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) )
71 oveq2 
 |-  ( ( # ` x ) = ( N + 2 ) -> ( 1 ... ( # ` x ) ) = ( 1 ... ( N + 2 ) ) )
72 71 eleq2d 
 |-  ( ( # ` x ) = ( N + 2 ) -> ( ( N + 1 ) e. ( 1 ... ( # ` x ) ) <-> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) ) )
73 72 ad2antrl 
 |-  ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( ( N + 1 ) e. ( 1 ... ( # ` x ) ) <-> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) ) )
74 70 73 mpbird 
 |-  ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( N + 1 ) e. ( 1 ... ( # ` x ) ) )
75 pfxfv0 
 |-  ( ( x e. Word V /\ ( N + 1 ) e. ( 1 ... ( # ` x ) ) ) -> ( ( x prefix ( N + 1 ) ) ` 0 ) = ( x ` 0 ) )
76 52 74 75 syl2anc 
 |-  ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( ( x prefix ( N + 1 ) ) ` 0 ) = ( x ` 0 ) )
77 76 ex 
 |-  ( N e. NN -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( ( x prefix ( N + 1 ) ) ` 0 ) = ( x ` 0 ) ) )
78 77 adantl 
 |-  ( ( X e. V /\ N e. NN ) -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( ( x prefix ( N + 1 ) ) ` 0 ) = ( x ` 0 ) ) )
79 78 impcom 
 |-  ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) -> ( ( x prefix ( N + 1 ) ) ` 0 ) = ( x ` 0 ) )
80 79 ad2antrl 
 |-  ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( x prefix ( N + 1 ) ) ` 0 ) = ( x ` 0 ) )
81 simpl 
 |-  ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( x ` 0 ) = X )
82 80 81 eqtrd 
 |-  ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( x prefix ( N + 1 ) ) ` 0 ) = X )
83 pfxfvlsw 
 |-  ( ( x e. Word V /\ ( N + 1 ) e. ( 1 ... ( # ` x ) ) ) -> ( lastS ` ( x prefix ( N + 1 ) ) ) = ( x ` ( ( N + 1 ) - 1 ) ) )
84 52 74 83 syl2anc 
 |-  ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( lastS ` ( x prefix ( N + 1 ) ) ) = ( x ` ( ( N + 1 ) - 1 ) ) )
85 27 42 syl 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) = N )
86 27 59 pncand 
 |-  ( N e. NN -> ( ( N + 2 ) - 2 ) = N )
87 85 86 eqtr4d 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) = ( ( N + 2 ) - 2 ) )
88 87 fveq2d 
 |-  ( N e. NN -> ( x ` ( ( N + 1 ) - 1 ) ) = ( x ` ( ( N + 2 ) - 2 ) ) )
89 88 adantr 
 |-  ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( x ` ( ( N + 1 ) - 1 ) ) = ( x ` ( ( N + 2 ) - 2 ) ) )
90 84 89 eqtr2d 
 |-  ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( x ` ( ( N + 2 ) - 2 ) ) = ( lastS ` ( x prefix ( N + 1 ) ) ) )
91 90 ex 
 |-  ( N e. NN -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( x ` ( ( N + 2 ) - 2 ) ) = ( lastS ` ( x prefix ( N + 1 ) ) ) ) )
92 91 adantl 
 |-  ( ( X e. V /\ N e. NN ) -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( x ` ( ( N + 2 ) - 2 ) ) = ( lastS ` ( x prefix ( N + 1 ) ) ) ) )
93 92 impcom 
 |-  ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) -> ( x ` ( ( N + 2 ) - 2 ) ) = ( lastS ` ( x prefix ( N + 1 ) ) ) )
94 93 neeq1d 
 |-  ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) -> ( ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) <-> ( lastS ` ( x prefix ( N + 1 ) ) ) =/= ( x ` 0 ) ) )
95 94 biimpcd 
 |-  ( ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) -> ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) -> ( lastS ` ( x prefix ( N + 1 ) ) ) =/= ( x ` 0 ) ) )
96 95 adantl 
 |-  ( ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) -> ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) -> ( lastS ` ( x prefix ( N + 1 ) ) ) =/= ( x ` 0 ) ) )
97 96 impcom 
 |-  ( ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( lastS ` ( x prefix ( N + 1 ) ) ) =/= ( x ` 0 ) )
98 97 adantl 
 |-  ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( lastS ` ( x prefix ( N + 1 ) ) ) =/= ( x ` 0 ) )
99 neeq2 
 |-  ( X = ( x ` 0 ) -> ( ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X <-> ( lastS ` ( x prefix ( N + 1 ) ) ) =/= ( x ` 0 ) ) )
100 99 eqcoms 
 |-  ( ( x ` 0 ) = X -> ( ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X <-> ( lastS ` ( x prefix ( N + 1 ) ) ) =/= ( x ` 0 ) ) )
101 100 adantr 
 |-  ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X <-> ( lastS ` ( x prefix ( N + 1 ) ) ) =/= ( x ` 0 ) ) )
102 98 101 mpbird 
 |-  ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X )
103 82 102 jca 
 |-  ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) )
104 51 103 mpancom 
 |-  ( ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) )
105 104 exp31 
 |-  ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( ( X e. V /\ N e. NN ) -> ( ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) -> ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) ) )
106 105 com23 
 |-  ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) -> ( ( X e. V /\ N e. NN ) -> ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) ) )
107 106 ancoms 
 |-  ( ( x e. Word V /\ ( # ` x ) = ( N + 2 ) ) -> ( ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) -> ( ( X e. V /\ N e. NN ) -> ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) ) )
108 50 107 syl 
 |-  ( x e. ( ( N + 2 ) ClWWalksN G ) -> ( ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) -> ( ( X e. V /\ N e. NN ) -> ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) ) )
109 108 imp 
 |-  ( ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( ( X e. V /\ N e. NN ) -> ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) )
110 109 com12 
 |-  ( ( X e. V /\ N e. NN ) -> ( ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) )
111 110 3adant1 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) )
112 111 imp 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) )
113 49 112 jca 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( x prefix ( N + 1 ) ) e. ( N WWalksN G ) /\ ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) )
114 113 ex 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( ( x prefix ( N + 1 ) ) e. ( N WWalksN G ) /\ ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) ) )
115 21 114 sylbid 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( x e. ( X H ( N + 2 ) ) -> ( ( x prefix ( N + 1 ) ) e. ( N WWalksN G ) /\ ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) ) )
116 115 imp 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( ( x prefix ( N + 1 ) ) e. ( N WWalksN G ) /\ ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) )
117 3simpc 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( X e. V /\ N e. NN ) )
118 117 adantr 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( X e. V /\ N e. NN ) )
119 1 2 numclwwlkovq 
 |-  ( ( X e. V /\ N e. NN ) -> ( X Q N ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } )
120 118 119 syl 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( X Q N ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } )
121 120 eleq2d 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( ( x prefix ( N + 1 ) ) e. ( X Q N ) <-> ( x prefix ( N + 1 ) ) e. { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } ) )
122 fveq1 
 |-  ( w = ( x prefix ( N + 1 ) ) -> ( w ` 0 ) = ( ( x prefix ( N + 1 ) ) ` 0 ) )
123 122 eqeq1d 
 |-  ( w = ( x prefix ( N + 1 ) ) -> ( ( w ` 0 ) = X <-> ( ( x prefix ( N + 1 ) ) ` 0 ) = X ) )
124 fveq2 
 |-  ( w = ( x prefix ( N + 1 ) ) -> ( lastS ` w ) = ( lastS ` ( x prefix ( N + 1 ) ) ) )
125 124 neeq1d 
 |-  ( w = ( x prefix ( N + 1 ) ) -> ( ( lastS ` w ) =/= X <-> ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) )
126 123 125 anbi12d 
 |-  ( w = ( x prefix ( N + 1 ) ) -> ( ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) <-> ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) )
127 126 elrab 
 |-  ( ( x prefix ( N + 1 ) ) e. { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } <-> ( ( x prefix ( N + 1 ) ) e. ( N WWalksN G ) /\ ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) )
128 121 127 bitrdi 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( ( x prefix ( N + 1 ) ) e. ( X Q N ) <-> ( ( x prefix ( N + 1 ) ) e. ( N WWalksN G ) /\ ( ( ( x prefix ( N + 1 ) ) ` 0 ) = X /\ ( lastS ` ( x prefix ( N + 1 ) ) ) =/= X ) ) ) )
129 116 128 mpbird 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( x prefix ( N + 1 ) ) e. ( X Q N ) )
130 129 4 fmptd 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> R : ( X H ( N + 2 ) ) --> ( X Q N ) )