Step |
Hyp |
Ref |
Expression |
1 |
|
eqeq1 |
|- ( y = x -> ( y = ( W cyclShift n ) <-> x = ( W cyclShift n ) ) ) |
2 |
1
|
rexbidv |
|- ( y = x -> ( E. n e. ( 0 ... N ) y = ( W cyclShift n ) <-> E. n e. ( 0 ... N ) x = ( W cyclShift n ) ) ) |
3 |
2
|
cbvrabv |
|- { y e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } = { x e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) x = ( W cyclShift n ) } |
4 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
5 |
4
|
clwwlknwrd |
|- ( w e. ( N ClWWalksN G ) -> w e. Word ( Vtx ` G ) ) |
6 |
5
|
ad2antrl |
|- ( ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) /\ ( w e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) -> w e. Word ( Vtx ` G ) ) |
7 |
|
simprr |
|- ( ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) /\ ( w e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) -> E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) |
8 |
6 7
|
jca |
|- ( ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) /\ ( w e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) -> ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) |
9 |
|
simprr |
|- ( ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) /\ ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) ) -> W e. ( N ClWWalksN G ) ) |
10 |
|
simpllr |
|- ( ( ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) /\ ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) ) /\ w = ( W cyclShift n ) ) -> n e. ( 0 ... N ) ) |
11 |
|
clwwnisshclwwsn |
|- ( ( W e. ( N ClWWalksN G ) /\ n e. ( 0 ... N ) ) -> ( W cyclShift n ) e. ( N ClWWalksN G ) ) |
12 |
9 10 11
|
syl2an2r |
|- ( ( ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) /\ ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) ) /\ w = ( W cyclShift n ) ) -> ( W cyclShift n ) e. ( N ClWWalksN G ) ) |
13 |
|
eleq1 |
|- ( w = ( W cyclShift n ) -> ( w e. ( N ClWWalksN G ) <-> ( W cyclShift n ) e. ( N ClWWalksN G ) ) ) |
14 |
13
|
adantl |
|- ( ( ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) /\ ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) ) /\ w = ( W cyclShift n ) ) -> ( w e. ( N ClWWalksN G ) <-> ( W cyclShift n ) e. ( N ClWWalksN G ) ) ) |
15 |
12 14
|
mpbird |
|- ( ( ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) /\ ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) ) /\ w = ( W cyclShift n ) ) -> w e. ( N ClWWalksN G ) ) |
16 |
15
|
exp31 |
|- ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) -> ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> ( w = ( W cyclShift n ) -> w e. ( N ClWWalksN G ) ) ) ) |
17 |
16
|
com23 |
|- ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) -> ( w = ( W cyclShift n ) -> ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> w e. ( N ClWWalksN G ) ) ) ) |
18 |
17
|
rexlimdva |
|- ( w e. Word ( Vtx ` G ) -> ( E. n e. ( 0 ... N ) w = ( W cyclShift n ) -> ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> w e. ( N ClWWalksN G ) ) ) ) |
19 |
18
|
imp |
|- ( ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) -> ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> w e. ( N ClWWalksN G ) ) ) |
20 |
19
|
impcom |
|- ( ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) /\ ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) -> w e. ( N ClWWalksN G ) ) |
21 |
|
simprr |
|- ( ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) /\ ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) -> E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) |
22 |
20 21
|
jca |
|- ( ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) /\ ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) -> ( w e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) |
23 |
8 22
|
impbida |
|- ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> ( ( w e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) <-> ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) ) |
24 |
|
eqeq1 |
|- ( x = w -> ( x = ( W cyclShift n ) <-> w = ( W cyclShift n ) ) ) |
25 |
24
|
rexbidv |
|- ( x = w -> ( E. n e. ( 0 ... N ) x = ( W cyclShift n ) <-> E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) |
26 |
25
|
elrab |
|- ( w e. { x e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) x = ( W cyclShift n ) } <-> ( w e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) |
27 |
|
eqeq1 |
|- ( y = w -> ( y = ( W cyclShift n ) <-> w = ( W cyclShift n ) ) ) |
28 |
27
|
rexbidv |
|- ( y = w -> ( E. n e. ( 0 ... N ) y = ( W cyclShift n ) <-> E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) |
29 |
28
|
elrab |
|- ( w e. { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } <-> ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) |
30 |
23 26 29
|
3bitr4g |
|- ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> ( w e. { x e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) x = ( W cyclShift n ) } <-> w e. { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } ) ) |
31 |
30
|
eqrdv |
|- ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> { x e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) x = ( W cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } ) |
32 |
3 31
|
syl5eq |
|- ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> { y e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } ) |