Metamath Proof Explorer


Theorem clwwlkwwlksb

Description: A nonempty word over vertices represents a closed walk iff the word concatenated with its first symbol represents a walk. (Contributed by AV, 4-Mar-2022)

Ref Expression
Hypothesis clwwlkwwlksb.v
|- V = ( Vtx ` G )
Assertion clwwlkwwlksb
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W e. ( ClWWalks ` G ) <-> ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) ) )

Proof

Step Hyp Ref Expression
1 clwwlkwwlksb.v
 |-  V = ( Vtx ` G )
2 fstwrdne
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W ` 0 ) e. V )
3 2 s1cld
 |-  ( ( W e. Word V /\ W =/= (/) ) -> <" ( W ` 0 ) "> e. Word V )
4 ccatlen
 |-  ( ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) -> ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( ( # ` W ) + ( # ` <" ( W ` 0 ) "> ) ) )
5 3 4 syldan
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( ( # ` W ) + ( # ` <" ( W ` 0 ) "> ) ) )
6 s1len
 |-  ( # ` <" ( W ` 0 ) "> ) = 1
7 6 oveq2i
 |-  ( ( # ` W ) + ( # ` <" ( W ` 0 ) "> ) ) = ( ( # ` W ) + 1 )
8 5 7 eqtrdi
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( ( # ` W ) + 1 ) )
9 8 oveq1d
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) = ( ( ( # ` W ) + 1 ) - 1 ) )
10 lencl
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
11 10 nn0cnd
 |-  ( W e. Word V -> ( # ` W ) e. CC )
12 11 adantr
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. CC )
13 1cnd
 |-  ( ( W e. Word V /\ W =/= (/) ) -> 1 e. CC )
14 12 13 13 addsubd
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( ( # ` W ) + 1 ) - 1 ) = ( ( ( # ` W ) - 1 ) + 1 ) )
15 9 14 eqtrd
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) = ( ( ( # ` W ) - 1 ) + 1 ) )
16 15 oveq2d
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) = ( 0 ..^ ( ( ( # ` W ) - 1 ) + 1 ) ) )
17 16 raleqdv
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( ( ( # ` W ) - 1 ) + 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
18 lennncl
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. NN )
19 nnm1nn0
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. NN0 )
20 18 19 syl
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. NN0 )
21 elnn0uz
 |-  ( ( ( # ` W ) - 1 ) e. NN0 <-> ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) )
22 20 21 sylib
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) )
23 fzosplitsn
 |-  ( ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( ( ( # ` W ) - 1 ) + 1 ) ) = ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) } ) )
24 22 23 syl
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( 0 ..^ ( ( ( # ` W ) - 1 ) + 1 ) ) = ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) } ) )
25 24 raleqdv
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( A. i e. ( 0 ..^ ( ( ( # ` W ) - 1 ) + 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) } ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
26 ralunb
 |-  ( A. i e. ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) } ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ A. i e. { ( ( # ` W ) - 1 ) } { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
27 25 26 bitrdi
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( A. i e. ( 0 ..^ ( ( ( # ` W ) - 1 ) + 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ A. i e. { ( ( # ` W ) - 1 ) } { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
28 simpl
 |-  ( ( W e. Word V /\ W =/= (/) ) -> W e. Word V )
29 10 nn0zd
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
30 29 adantr
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. ZZ )
31 elfzom1elfzo
 |-  ( ( ( # ` W ) e. ZZ /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> i e. ( 0 ..^ ( # ` W ) ) )
32 30 31 sylan
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> i e. ( 0 ..^ ( # ` W ) ) )
33 ccats1val1
 |-  ( ( W e. Word V /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` i ) = ( W ` i ) )
34 28 32 33 syl2an2r
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` i ) = ( W ` i ) )
35 elfzom1elp1fzo
 |-  ( ( ( # ` W ) e. ZZ /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) )
36 30 35 sylan
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) )
37 ccats1val1
 |-  ( ( W e. Word V /\ ( i + 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
38 28 36 37 syl2an2r
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
39 34 38 preq12d
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } )
40 39 eleq1d
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
41 40 ralbidva
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
42 ovex
 |-  ( ( # ` W ) - 1 ) e. _V
43 fveq2
 |-  ( i = ( ( # ` W ) - 1 ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` i ) = ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) )
44 fvoveq1
 |-  ( i = ( ( # ` W ) - 1 ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) = ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) )
45 43 44 preq12d
 |-  ( i = ( ( # ` W ) - 1 ) -> { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } = { ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } )
46 45 eleq1d
 |-  ( i = ( ( # ` W ) - 1 ) -> ( { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. ( Edg ` G ) ) )
47 42 46 ralsn
 |-  ( A. i e. { ( ( # ` W ) - 1 ) } { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. ( Edg ` G ) )
48 fzo0end
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
49 18 48 syl
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
50 ccats1val1
 |-  ( ( W e. Word V /\ ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) = ( W ` ( ( # ` W ) - 1 ) ) )
51 49 50 syldan
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) = ( W ` ( ( # ` W ) - 1 ) ) )
52 lsw
 |-  ( W e. Word V -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
53 52 adantr
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
54 51 53 eqtr4d
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) = ( lastS ` W ) )
55 npcan1
 |-  ( ( # ` W ) e. CC -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
56 11 55 syl
 |-  ( W e. Word V -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
57 56 adantr
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
58 57 fveq2d
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) = ( ( W ++ <" ( W ` 0 ) "> ) ` ( # ` W ) ) )
59 eqidd
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) = ( # ` W ) )
60 ccats1val2
 |-  ( ( W e. Word V /\ ( W ` 0 ) e. V /\ ( # ` W ) = ( # ` W ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( # ` W ) ) = ( W ` 0 ) )
61 28 2 59 60 syl3anc
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( # ` W ) ) = ( W ` 0 ) )
62 58 61 eqtrd
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) = ( W ` 0 ) )
63 54 62 preq12d
 |-  ( ( W e. Word V /\ W =/= (/) ) -> { ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } = { ( lastS ` W ) , ( W ` 0 ) } )
64 63 eleq1d
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( { ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( # ` W ) - 1 ) ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. ( Edg ` G ) <-> { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
65 47 64 syl5bb
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( A. i e. { ( ( # ` W ) - 1 ) } { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
66 41 65 anbi12d
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ A. i e. { ( ( # ` W ) - 1 ) } { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
67 17 27 66 3bitrd
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
68 28 3 jca
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) )
69 ccat0
 |-  ( ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) -> ( ( W ++ <" ( W ` 0 ) "> ) = (/) <-> ( W = (/) /\ <" ( W ` 0 ) "> = (/) ) ) )
70 simpl
 |-  ( ( W = (/) /\ <" ( W ` 0 ) "> = (/) ) -> W = (/) )
71 69 70 syl6bi
 |-  ( ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) -> ( ( W ++ <" ( W ` 0 ) "> ) = (/) -> W = (/) ) )
72 71 necon3d
 |-  ( ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) -> ( W =/= (/) -> ( W ++ <" ( W ` 0 ) "> ) =/= (/) ) )
73 72 adantld
 |-  ( ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) -> ( ( W e. Word V /\ W =/= (/) ) -> ( W ++ <" ( W ` 0 ) "> ) =/= (/) ) )
74 68 73 mpcom
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W ++ <" ( W ` 0 ) "> ) =/= (/) )
75 wrdv
 |-  ( W e. Word V -> W e. Word _V )
76 s1cli
 |-  <" ( W ` 0 ) "> e. Word _V
77 ccatalpha
 |-  ( ( W e. Word _V /\ <" ( W ` 0 ) "> e. Word _V ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. Word V <-> ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) ) )
78 75 76 77 sylancl
 |-  ( W e. Word V -> ( ( W ++ <" ( W ` 0 ) "> ) e. Word V <-> ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) ) )
79 78 adantr
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. Word V <-> ( W e. Word V /\ <" ( W ` 0 ) "> e. Word V ) ) )
80 28 3 79 mpbir2and
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W ++ <" ( W ` 0 ) "> ) e. Word V )
81 74 80 jca
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) =/= (/) /\ ( W ++ <" ( W ` 0 ) "> ) e. Word V ) )
82 eqid
 |-  ( Edg ` G ) = ( Edg ` G )
83 1 82 iswwlks
 |-  ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) <-> ( ( W ++ <" ( W ` 0 ) "> ) =/= (/) /\ ( W ++ <" ( W ` 0 ) "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
84 df-3an
 |-  ( ( ( W ++ <" ( W ` 0 ) "> ) =/= (/) /\ ( W ++ <" ( W ` 0 ) "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> ( ( ( W ++ <" ( W ` 0 ) "> ) =/= (/) /\ ( W ++ <" ( W ` 0 ) "> ) e. Word V ) /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
85 83 84 bitri
 |-  ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) <-> ( ( ( W ++ <" ( W ` 0 ) "> ) =/= (/) /\ ( W ++ <" ( W ` 0 ) "> ) e. Word V ) /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
86 85 a1i
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) <-> ( ( ( W ++ <" ( W ` 0 ) "> ) =/= (/) /\ ( W ++ <" ( W ` 0 ) "> ) e. Word V ) /\ A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
87 81 86 mpbirand
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) <-> A. i e. ( 0 ..^ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) { ( ( W ++ <" ( W ` 0 ) "> ) ` i ) , ( ( W ++ <" ( W ` 0 ) "> ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
88 1 82 isclwwlk
 |-  ( W e. ( ClWWalks ` G ) <-> ( ( W e. Word V /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
89 3anass
 |-  ( ( ( W e. Word V /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( ( W e. Word V /\ W =/= (/) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
90 88 89 bitri
 |-  ( W e. ( ClWWalks ` G ) <-> ( ( W e. Word V /\ W =/= (/) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
91 90 baib
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W e. ( ClWWalks ` G ) <-> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
92 67 87 91 3bitr4rd
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W e. ( ClWWalks ` G ) <-> ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) ) )