Step |
Hyp |
Ref |
Expression |
1 |
|
clwwlkwwlksb.v |
|- V = ( Vtx ` G ) |
2 |
|
nnnn0 |
|- ( N e. NN -> N e. NN0 ) |
3 |
|
ccatws1lenp1b |
|- ( ( W e. Word V /\ N e. NN0 ) -> ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( N + 1 ) <-> ( # ` W ) = N ) ) |
4 |
2 3
|
sylan2 |
|- ( ( W e. Word V /\ N e. NN ) -> ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( N + 1 ) <-> ( # ` W ) = N ) ) |
5 |
4
|
anbi2d |
|- ( ( W e. Word V /\ N e. NN ) -> ( ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( N + 1 ) ) <-> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` W ) = N ) ) ) |
6 |
|
simpl |
|- ( ( W e. Word V /\ N e. NN ) -> W e. Word V ) |
7 |
|
eleq1 |
|- ( ( # ` W ) = N -> ( ( # ` W ) e. NN <-> N e. NN ) ) |
8 |
|
len0nnbi |
|- ( W e. Word V -> ( W =/= (/) <-> ( # ` W ) e. NN ) ) |
9 |
8
|
biimprcd |
|- ( ( # ` W ) e. NN -> ( W e. Word V -> W =/= (/) ) ) |
10 |
7 9
|
syl6bir |
|- ( ( # ` W ) = N -> ( N e. NN -> ( W e. Word V -> W =/= (/) ) ) ) |
11 |
10
|
com13 |
|- ( W e. Word V -> ( N e. NN -> ( ( # ` W ) = N -> W =/= (/) ) ) ) |
12 |
11
|
imp31 |
|- ( ( ( W e. Word V /\ N e. NN ) /\ ( # ` W ) = N ) -> W =/= (/) ) |
13 |
1
|
clwwlkwwlksb |
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W e. ( ClWWalks ` G ) <-> ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) ) ) |
14 |
6 12 13
|
syl2an2r |
|- ( ( ( W e. Word V /\ N e. NN ) /\ ( # ` W ) = N ) -> ( W e. ( ClWWalks ` G ) <-> ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) ) ) |
15 |
14
|
bicomd |
|- ( ( ( W e. Word V /\ N e. NN ) /\ ( # ` W ) = N ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) <-> W e. ( ClWWalks ` G ) ) ) |
16 |
15
|
ex |
|- ( ( W e. Word V /\ N e. NN ) -> ( ( # ` W ) = N -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) <-> W e. ( ClWWalks ` G ) ) ) ) |
17 |
16
|
pm5.32rd |
|- ( ( W e. Word V /\ N e. NN ) -> ( ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` W ) = N ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) ) ) |
18 |
5 17
|
bitrd |
|- ( ( W e. Word V /\ N e. NN ) -> ( ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( N + 1 ) ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) ) ) |
19 |
2
|
adantl |
|- ( ( W e. Word V /\ N e. NN ) -> N e. NN0 ) |
20 |
|
iswwlksn |
|- ( N e. NN0 -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) <-> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( N + 1 ) ) ) ) |
21 |
19 20
|
syl |
|- ( ( W e. Word V /\ N e. NN ) -> ( ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) <-> ( ( W ++ <" ( W ` 0 ) "> ) e. ( WWalks ` G ) /\ ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( N + 1 ) ) ) ) |
22 |
|
isclwwlkn |
|- ( W e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) ) |
23 |
22
|
a1i |
|- ( ( W e. Word V /\ N e. NN ) -> ( W e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) ) ) |
24 |
18 21 23
|
3bitr4rd |
|- ( ( W e. Word V /\ N e. NN ) -> ( W e. ( N ClWWalksN G ) <-> ( W ++ <" ( W ` 0 ) "> ) e. ( N WWalksN G ) ) ) |