Metamath Proof Explorer

Theorem clwwlknonwwlknonb

Description: A word over vertices represents a closed walk of a fixed length N on vertex X iff the word concatenated with X represents a walk of length N on X and X . This theorem would not hold for N = 0 and W = (/) , see clwwlknwwlksnb . (Contributed by AV, 4-Mar-2022) (Revised by AV, 27-Mar-2022)

Ref Expression
Hypothesis clwwlknonwwlknonb.v 
|- V = ( Vtx ` G )
Assertion clwwlknonwwlknonb 
|- ( ( W e. Word V /\ N e. NN ) -> ( W e. ( X ( ClWWalksNOn ` G ) N ) <-> ( W ++ <" X "> ) e. ( X ( N WWalksNOn G ) X ) ) )

Proof

Step Hyp Ref Expression
1 clwwlknonwwlknonb.v 
 |-  V = ( Vtx ` G )
2 isclwwlknon 
 |-  ( W e. ( X ( ClWWalksNOn ` G ) N ) <-> ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) )
3 3anan32 
 |-  ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` 0 ) = X /\ ( ( W ++ <" X "> ) ` N ) = X ) <-> ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` N ) = X ) /\ ( ( W ++ <" X "> ) ` 0 ) = X ) )
4 s1eq 
 |-  ( ( W ` 0 ) = X -> <" ( W ` 0 ) "> = <" X "> )
5 4 oveq2d 
 |-  ( ( W ` 0 ) = X -> ( W ++ <" ( W ` 0 ) "> ) = ( W ++ <" X "> ) )
6 5 eleq1d 
 |-  ( ( W ` 0 ) = X -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) <-> ( W ++ <" X "> ) e. ( N WWalksN G ) ) )
7 6 biimpac 
 |-  ( ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) -> ( W ++ <" X "> ) e. ( N WWalksN G ) )
8 7 adantl 
 |-  ( ( ( W e. Word V /\ N e. NN ) /\ ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) ) -> ( W ++ <" X "> ) e. ( N WWalksN G ) )
9 fvex 
 |-  ( W ` 0 ) e. _V
10 eleq1 
 |-  ( ( W ` 0 ) = X -> ( ( W ` 0 ) e. _V <-> X e. _V ) )
11 9 10 mpbii 
 |-  ( ( W ` 0 ) = X -> X e. _V )
12 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
13 1 12 wwlknp 
 |-  ( ( W ++ <" X "> ) e. ( N WWalksN G ) -> ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( ( W ++ <" X "> ) ` i ) , ( ( W ++ <" X "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
14 simprrl 
 |-  ( ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) /\ ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) ) -> W e. Word V )
15 simpl 
 |-  ( ( W e. Word V /\ N e. NN ) -> W e. Word V )
16 15 anim2i 
 |-  ( ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) -> ( X e. _V /\ W e. Word V ) )
17 16 ancomd 
 |-  ( ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) -> ( W e. Word V /\ X e. _V ) )
18 ccats1alpha 
 |-  ( ( W e. Word V /\ X e. _V ) -> ( ( W ++ <" X "> ) e. Word V <-> ( W e. Word V /\ X e. V ) ) )
19 17 18 syl 
 |-  ( ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) -> ( ( W ++ <" X "> ) e. Word V <-> ( W e. Word V /\ X e. V ) ) )
20 simpr 
 |-  ( ( W e. Word V /\ X e. V ) -> X e. V )
21 19 20 biimtrdi 
 |-  ( ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) -> ( ( W ++ <" X "> ) e. Word V -> X e. V ) )
22 21 com12 
 |-  ( ( W ++ <" X "> ) e. Word V -> ( ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) -> X e. V ) )
23 22 adantr 
 |-  ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) -> ( ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) -> X e. V ) )
24 23 imp 
 |-  ( ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) /\ ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) ) -> X e. V )
25 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
26 ccatws1lenp1b 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) <-> ( # ` W ) = N ) )
27 25 26 sylan2 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) <-> ( # ` W ) = N ) )
28 27 biimpd 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) -> ( # ` W ) = N ) )
29 28 adantl 
 |-  ( ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) -> ( ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) -> ( # ` W ) = N ) )
30 29 com12 
 |-  ( ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) -> ( ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) -> ( # ` W ) = N ) )
31 30 adantl 
 |-  ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) -> ( ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) -> ( # ` W ) = N ) )
32 31 imp 
 |-  ( ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) /\ ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) ) -> ( # ` W ) = N )
33 32 eqcomd 
 |-  ( ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) /\ ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) ) -> N = ( # ` W ) )
34 14 24 33 3jca 
 |-  ( ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) /\ ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) ) -> ( W e. Word V /\ X e. V /\ N = ( # ` W ) ) )
35 34 ex 
 |-  ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) -> ( ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) -> ( W e. Word V /\ X e. V /\ N = ( # ` W ) ) ) )
36 35 3adant3 
 |-  ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( ( W ++ <" X "> ) ` i ) , ( ( W ++ <" X "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) -> ( W e. Word V /\ X e. V /\ N = ( # ` W ) ) ) )
37 13 36 syl 
 |-  ( ( W ++ <" X "> ) e. ( N WWalksN G ) -> ( ( X e. _V /\ ( W e. Word V /\ N e. NN ) ) -> ( W e. Word V /\ X e. V /\ N = ( # ` W ) ) ) )
38 37 expd 
 |-  ( ( W ++ <" X "> ) e. ( N WWalksN G ) -> ( X e. _V -> ( ( W e. Word V /\ N e. NN ) -> ( W e. Word V /\ X e. V /\ N = ( # ` W ) ) ) ) )
39 11 38 syl5com 
 |-  ( ( W ` 0 ) = X -> ( ( W ++ <" X "> ) e. ( N WWalksN G ) -> ( ( W e. Word V /\ N e. NN ) -> ( W e. Word V /\ X e. V /\ N = ( # ` W ) ) ) ) )
40 6 39 sylbid 
 |-  ( ( W ` 0 ) = X -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) -> ( ( W e. Word V /\ N e. NN ) -> ( W e. Word V /\ X e. V /\ N = ( # ` W ) ) ) ) )
41 40 com13 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) -> ( ( W ` 0 ) = X -> ( W e. Word V /\ X e. V /\ N = ( # ` W ) ) ) ) )
42 41 imp32 
 |-  ( ( ( W e. Word V /\ N e. NN ) /\ ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) ) -> ( W e. Word V /\ X e. V /\ N = ( # ` W ) ) )
43 ccats1val2 
 |-  ( ( W e. Word V /\ X e. V /\ N = ( # ` W ) ) -> ( ( W ++ <" X "> ) ` N ) = X )
44 42 43 syl 
 |-  ( ( ( W e. Word V /\ N e. NN ) /\ ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) ) -> ( ( W ++ <" X "> ) ` N ) = X )
45 ccat1st1st 
 |-  ( W e. Word V -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) )
46 45 adantr 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) )
47 5 fveq1d 
 |-  ( ( W ` 0 ) = X -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( ( W ++ <" X "> ) ` 0 ) )
48 47 eqeq1d 
 |-  ( ( W ` 0 ) = X -> ( ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) <-> ( ( W ++ <" X "> ) ` 0 ) = ( W ` 0 ) ) )
49 48 adantl 
 |-  ( ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) -> ( ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) <-> ( ( W ++ <" X "> ) ` 0 ) = ( W ` 0 ) ) )
50 46 49 syl5ibcom 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) -> ( ( W ++ <" X "> ) ` 0 ) = ( W ` 0 ) ) )
51 50 imp 
 |-  ( ( ( W e. Word V /\ N e. NN ) /\ ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) ) -> ( ( W ++ <" X "> ) ` 0 ) = ( W ` 0 ) )
52 simprr 
 |-  ( ( ( W e. Word V /\ N e. NN ) /\ ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) ) -> ( W ` 0 ) = X )
53 51 52 eqtrd 
 |-  ( ( ( W e. Word V /\ N e. NN ) /\ ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) ) -> ( ( W ++ <" X "> ) ` 0 ) = X )
54 8 44 53 jca31 
 |-  ( ( ( W e. Word V /\ N e. NN ) /\ ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) ) -> ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` N ) = X ) /\ ( ( W ++ <" X "> ) ` 0 ) = X ) )
55 54 ex 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) -> ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` N ) = X ) /\ ( ( W ++ <" X "> ) ` 0 ) = X ) ) )
56 simprl 
 |-  ( ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) /\ ( W e. Word V /\ N e. NN ) ) -> W e. Word V )
57 27 biimpcd 
 |-  ( ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) -> ( ( W e. Word V /\ N e. NN ) -> ( # ` W ) = N ) )
58 57 adantl 
 |-  ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) -> ( ( W e. Word V /\ N e. NN ) -> ( # ` W ) = N ) )
59 58 imp 
 |-  ( ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) /\ ( W e. Word V /\ N e. NN ) ) -> ( # ` W ) = N )
60 59 eqcomd 
 |-  ( ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) /\ ( W e. Word V /\ N e. NN ) ) -> N = ( # ` W ) )
61 56 60 jca 
 |-  ( ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) /\ ( W e. Word V /\ N e. NN ) ) -> ( W e. Word V /\ N = ( # ` W ) ) )
62 61 ex 
 |-  ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) -> ( ( W e. Word V /\ N e. NN ) -> ( W e. Word V /\ N = ( # ` W ) ) ) )
63 62 3adant3 
 |-  ( ( ( W ++ <" X "> ) e. Word V /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( ( W ++ <" X "> ) ` i ) , ( ( W ++ <" X "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( W e. Word V /\ N e. NN ) -> ( W e. Word V /\ N = ( # ` W ) ) ) )
64 13 63 syl 
 |-  ( ( W ++ <" X "> ) e. ( N WWalksN G ) -> ( ( W e. Word V /\ N e. NN ) -> ( W e. Word V /\ N = ( # ` W ) ) ) )
65 64 imp 
 |-  ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( W e. Word V /\ N e. NN ) ) -> ( W e. Word V /\ N = ( # ` W ) ) )
66 eleq1 
 |-  ( N = ( # ` W ) -> ( N e. NN <-> ( # ` W ) e. NN ) )
67 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` W ) ) <-> ( # ` W ) e. NN )
68 67 biimpri 
 |-  ( ( # ` W ) e. NN -> 0 e. ( 0 ..^ ( # ` W ) ) )
69 66 68 biimtrdi 
 |-  ( N = ( # ` W ) -> ( N e. NN -> 0 e. ( 0 ..^ ( # ` W ) ) ) )
70 69 com12 
 |-  ( N e. NN -> ( N = ( # ` W ) -> 0 e. ( 0 ..^ ( # ` W ) ) ) )
71 70 ad2antll 
 |-  ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( W e. Word V /\ N e. NN ) ) -> ( N = ( # ` W ) -> 0 e. ( 0 ..^ ( # ` W ) ) ) )
72 71 anim2d 
 |-  ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( W e. Word V /\ N e. NN ) ) -> ( ( W e. Word V /\ N = ( # ` W ) ) -> ( W e. Word V /\ 0 e. ( 0 ..^ ( # ` W ) ) ) ) )
73 65 72 mpd 
 |-  ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( W e. Word V /\ N e. NN ) ) -> ( W e. Word V /\ 0 e. ( 0 ..^ ( # ` W ) ) ) )
74 ccats1val1 
 |-  ( ( W e. Word V /\ 0 e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" X "> ) ` 0 ) = ( W ` 0 ) )
75 73 74 syl 
 |-  ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( W e. Word V /\ N e. NN ) ) -> ( ( W ++ <" X "> ) ` 0 ) = ( W ` 0 ) )
76 75 eqeq1d 
 |-  ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( W e. Word V /\ N e. NN ) ) -> ( ( ( W ++ <" X "> ) ` 0 ) = X <-> ( W ` 0 ) = X ) )
77 76 biimpd 
 |-  ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( W e. Word V /\ N e. NN ) ) -> ( ( ( W ++ <" X "> ) ` 0 ) = X -> ( W ` 0 ) = X ) )
78 77 ex 
 |-  ( ( W ++ <" X "> ) e. ( N WWalksN G ) -> ( ( W e. Word V /\ N e. NN ) -> ( ( ( W ++ <" X "> ) ` 0 ) = X -> ( W ` 0 ) = X ) ) )
79 78 adantr 
 |-  ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` N ) = X ) -> ( ( W e. Word V /\ N e. NN ) -> ( ( ( W ++ <" X "> ) ` 0 ) = X -> ( W ` 0 ) = X ) ) )
80 79 com3r 
 |-  ( ( ( W ++ <" X "> ) ` 0 ) = X -> ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` N ) = X ) -> ( ( W e. Word V /\ N e. NN ) -> ( W ` 0 ) = X ) ) )
81 80 impcom 
 |-  ( ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` N ) = X ) /\ ( ( W ++ <" X "> ) ` 0 ) = X ) -> ( ( W e. Word V /\ N e. NN ) -> ( W ` 0 ) = X ) )
82 6 biimparc 
 |-  ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) -> ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) )
83 simpr 
 |-  ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) -> ( W ` 0 ) = X )
84 82 83 jca 
 |-  ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) )
85 84 ex 
 |-  ( ( W ++ <" X "> ) e. ( N WWalksN G ) -> ( ( W ` 0 ) = X -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) ) )
86 85 ad2antrr 
 |-  ( ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` N ) = X ) /\ ( ( W ++ <" X "> ) ` 0 ) = X ) -> ( ( W ` 0 ) = X -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) ) )
87 81 86 syldc 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` N ) = X ) /\ ( ( W ++ <" X "> ) ` 0 ) = X ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) ) )
88 55 87 impbid 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) <-> ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` N ) = X ) /\ ( ( W ++ <" X "> ) ` 0 ) = X ) ) )
89 3 88 bitr4id 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` 0 ) = X /\ ( ( W ++ <" X "> ) ` N ) = X ) <-> ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) ) )
90 1 clwwlknwwlksnb 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( W e. ( N ClWWalksN G ) <-> ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) ) )
91 90 anbi1d 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) <-> ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) /\ ( W ` 0 ) = X ) ) )
92 89 91 bitr4d 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` 0 ) = X /\ ( ( W ++ <" X "> ) ` N ) = X ) <-> ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) ) )
93 2 92 bitr4id 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( W e. ( X ( ClWWalksNOn ` G ) N ) <-> ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` 0 ) = X /\ ( ( W ++ <" X "> ) ` N ) = X ) ) )
94 wwlknon 
 |-  ( ( W ++ <" X "> ) e. ( X ( N WWalksNOn G ) X ) <-> ( ( W ++ <" X "> ) e. ( N WWalksN G ) /\ ( ( W ++ <" X "> ) ` 0 ) = X /\ ( ( W ++ <" X "> ) ` N ) = X ) )
95 93 94 bitr4di 
 |-  ( ( W e. Word V /\ N e. NN ) -> ( W e. ( X ( ClWWalksNOn ` G ) N ) <-> ( W ++ <" X "> ) e. ( X ( N WWalksNOn G ) X ) ) )