Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
2 |
1
|
wwlkbp |
|- ( W e. ( WWalks ` G ) -> ( G e. _V /\ W e. Word ( Vtx ` G ) ) ) |
3 |
2
|
simprd |
|- ( W e. ( WWalks ` G ) -> W e. Word ( Vtx ` G ) ) |
4 |
1
|
wwlkbp |
|- ( T e. ( WWalks ` G ) -> ( G e. _V /\ T e. Word ( Vtx ` G ) ) ) |
5 |
4
|
simprd |
|- ( T e. ( WWalks ` G ) -> T e. Word ( Vtx ` G ) ) |
6 |
|
eqwrd |
|- ( ( W e. Word ( Vtx ` G ) /\ T e. Word ( Vtx ` G ) ) -> ( W = T <-> ( ( # ` W ) = ( # ` T ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( T ` i ) ) ) ) |
7 |
3 5 6
|
syl2an |
|- ( ( W e. ( WWalks ` G ) /\ T e. ( WWalks ` G ) ) -> ( W = T <-> ( ( # ` W ) = ( # ` T ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( T ` i ) ) ) ) |