Step |
Hyp |
Ref |
Expression |
1 |
|
2nn |
|- 2 e. NN |
2 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
3 |
|
eqid |
|- ( Edg ` G ) = ( Edg ` G ) |
4 |
2 3
|
isclwwlknx |
|- ( 2 e. NN -> ( W e. ( 2 ClWWalksN G ) <-> ( ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 2 ) ) ) |
5 |
1 4
|
ax-mp |
|- ( W e. ( 2 ClWWalksN G ) <-> ( ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 2 ) ) |
6 |
|
3anass |
|- ( ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( W e. Word ( Vtx ` G ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) ) |
7 |
|
oveq1 |
|- ( ( # ` W ) = 2 -> ( ( # ` W ) - 1 ) = ( 2 - 1 ) ) |
8 |
|
2m1e1 |
|- ( 2 - 1 ) = 1 |
9 |
7 8
|
eqtrdi |
|- ( ( # ` W ) = 2 -> ( ( # ` W ) - 1 ) = 1 ) |
10 |
9
|
oveq2d |
|- ( ( # ` W ) = 2 -> ( 0 ..^ ( ( # ` W ) - 1 ) ) = ( 0 ..^ 1 ) ) |
11 |
|
fzo01 |
|- ( 0 ..^ 1 ) = { 0 } |
12 |
10 11
|
eqtrdi |
|- ( ( # ` W ) = 2 -> ( 0 ..^ ( ( # ` W ) - 1 ) ) = { 0 } ) |
13 |
12
|
adantr |
|- ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( 0 ..^ ( ( # ` W ) - 1 ) ) = { 0 } ) |
14 |
13
|
raleqdv |
|- ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. { 0 } { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) |
15 |
|
c0ex |
|- 0 e. _V |
16 |
|
fveq2 |
|- ( i = 0 -> ( W ` i ) = ( W ` 0 ) ) |
17 |
|
fv0p1e1 |
|- ( i = 0 -> ( W ` ( i + 1 ) ) = ( W ` 1 ) ) |
18 |
16 17
|
preq12d |
|- ( i = 0 -> { ( W ` i ) , ( W ` ( i + 1 ) ) } = { ( W ` 0 ) , ( W ` 1 ) } ) |
19 |
18
|
eleq1d |
|- ( i = 0 -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) |
20 |
15 19
|
ralsn |
|- ( A. i e. { 0 } { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) |
21 |
14 20
|
bitrdi |
|- ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) |
22 |
|
prcom |
|- { ( lastS ` W ) , ( W ` 0 ) } = { ( W ` 0 ) , ( lastS ` W ) } |
23 |
|
lsw |
|- ( W e. Word ( Vtx ` G ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) ) |
24 |
9
|
fveq2d |
|- ( ( # ` W ) = 2 -> ( W ` ( ( # ` W ) - 1 ) ) = ( W ` 1 ) ) |
25 |
23 24
|
sylan9eqr |
|- ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( lastS ` W ) = ( W ` 1 ) ) |
26 |
25
|
preq2d |
|- ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> { ( W ` 0 ) , ( lastS ` W ) } = { ( W ` 0 ) , ( W ` 1 ) } ) |
27 |
22 26
|
syl5eq |
|- ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> { ( lastS ` W ) , ( W ` 0 ) } = { ( W ` 0 ) , ( W ` 1 ) } ) |
28 |
27
|
eleq1d |
|- ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) <-> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) |
29 |
21 28
|
anbi12d |
|- ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) ) |
30 |
|
anidm |
|- ( ( { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) <-> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) |
31 |
29 30
|
bitrdi |
|- ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) <-> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) |
32 |
31
|
pm5.32da |
|- ( ( # ` W ) = 2 -> ( ( W e. Word ( Vtx ` G ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) <-> ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) ) |
33 |
6 32
|
syl5bb |
|- ( ( # ` W ) = 2 -> ( ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) ) |
34 |
33
|
pm5.32ri |
|- ( ( ( W e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 2 ) <-> ( ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 2 ) ) |
35 |
|
3anass |
|- ( ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) <-> ( ( # ` W ) = 2 /\ ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) ) |
36 |
|
ancom |
|- ( ( ( # ` W ) = 2 /\ ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) <-> ( ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 2 ) ) |
37 |
35 36
|
bitr2i |
|- ( ( ( W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) /\ ( # ` W ) = 2 ) <-> ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) |
38 |
5 34 37
|
3bitri |
|- ( W e. ( 2 ClWWalksN G ) <-> ( ( # ` W ) = 2 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) ) |