Step |
Hyp |
Ref |
Expression |
1 |
|
extwwlkfab.v |
|- V = ( Vtx ` G ) |
2 |
|
extwwlkfab.c |
|- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) |
3 |
|
extwwlkfab.f |
|- F = ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) |
4 |
1 2 3
|
extwwlkfab |
|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( X C N ) = { w e. ( N ClWWalksN G ) | ( ( w prefix ( N - 2 ) ) e. F /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) } ) |
5 |
4
|
eleq2d |
|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X C N ) <-> W e. { w e. ( N ClWWalksN G ) | ( ( w prefix ( N - 2 ) ) e. F /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) } ) ) |
6 |
|
oveq1 |
|- ( w = W -> ( w prefix ( N - 2 ) ) = ( W prefix ( N - 2 ) ) ) |
7 |
6
|
eleq1d |
|- ( w = W -> ( ( w prefix ( N - 2 ) ) e. F <-> ( W prefix ( N - 2 ) ) e. F ) ) |
8 |
|
fveq1 |
|- ( w = W -> ( w ` ( N - 1 ) ) = ( W ` ( N - 1 ) ) ) |
9 |
8
|
eleq1d |
|- ( w = W -> ( ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) <-> ( W ` ( N - 1 ) ) e. ( G NeighbVtx X ) ) ) |
10 |
|
fveq1 |
|- ( w = W -> ( w ` ( N - 2 ) ) = ( W ` ( N - 2 ) ) ) |
11 |
10
|
eqeq1d |
|- ( w = W -> ( ( w ` ( N - 2 ) ) = X <-> ( W ` ( N - 2 ) ) = X ) ) |
12 |
7 9 11
|
3anbi123d |
|- ( w = W -> ( ( ( w prefix ( N - 2 ) ) e. F /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) <-> ( ( W prefix ( N - 2 ) ) e. F /\ ( W ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( W ` ( N - 2 ) ) = X ) ) ) |
13 |
12
|
elrab |
|- ( W e. { w e. ( N ClWWalksN G ) | ( ( w prefix ( N - 2 ) ) e. F /\ ( w ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( w ` ( N - 2 ) ) = X ) } <-> ( W e. ( N ClWWalksN G ) /\ ( ( W prefix ( N - 2 ) ) e. F /\ ( W ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( W ` ( N - 2 ) ) = X ) ) ) |
14 |
5 13
|
syl6bb |
|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X C N ) <-> ( W e. ( N ClWWalksN G ) /\ ( ( W prefix ( N - 2 ) ) e. F /\ ( W ` ( N - 1 ) ) e. ( G NeighbVtx X ) /\ ( W ` ( N - 2 ) ) = X ) ) ) ) |