Step |
Hyp |
Ref |
Expression |
1 |
|
clwwlknun.v |
|- V = ( Vtx ` G ) |
2 |
|
eliun |
|- ( y e. U_ x e. V ( x ( ClWWalksNOn ` G ) N ) <-> E. x e. V y e. ( x ( ClWWalksNOn ` G ) N ) ) |
3 |
|
isclwwlknon |
|- ( y e. ( x ( ClWWalksNOn ` G ) N ) <-> ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) ) |
4 |
3
|
rexbii |
|- ( E. x e. V y e. ( x ( ClWWalksNOn ` G ) N ) <-> E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) ) |
5 |
|
simpl |
|- ( ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) -> y e. ( N ClWWalksN G ) ) |
6 |
5
|
rexlimivw |
|- ( E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) -> y e. ( N ClWWalksN G ) ) |
7 |
|
eqid |
|- ( Edg ` G ) = ( Edg ` G ) |
8 |
1 7
|
clwwlknp |
|- ( y e. ( N ClWWalksN G ) -> ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) |
9 |
8
|
anim2i |
|- ( ( G e. USGraph /\ y e. ( N ClWWalksN G ) ) -> ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) ) |
10 |
7 1
|
usgrpredgv |
|- ( ( G e. USGraph /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) -> ( ( lastS ` y ) e. V /\ ( y ` 0 ) e. V ) ) |
11 |
10
|
ex |
|- ( G e. USGraph -> ( { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) -> ( ( lastS ` y ) e. V /\ ( y ` 0 ) e. V ) ) ) |
12 |
|
simpr |
|- ( ( ( lastS ` y ) e. V /\ ( y ` 0 ) e. V ) -> ( y ` 0 ) e. V ) |
13 |
11 12
|
syl6com |
|- ( { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) -> ( G e. USGraph -> ( y ` 0 ) e. V ) ) |
14 |
13
|
3ad2ant3 |
|- ( ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) -> ( G e. USGraph -> ( y ` 0 ) e. V ) ) |
15 |
14
|
impcom |
|- ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) -> ( y ` 0 ) e. V ) |
16 |
|
simpr |
|- ( ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) /\ x = ( y ` 0 ) ) -> x = ( y ` 0 ) ) |
17 |
16
|
eqcomd |
|- ( ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) /\ x = ( y ` 0 ) ) -> ( y ` 0 ) = x ) |
18 |
17
|
biantrud |
|- ( ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) /\ x = ( y ` 0 ) ) -> ( y e. ( N ClWWalksN G ) <-> ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) ) ) |
19 |
18
|
bicomd |
|- ( ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) /\ x = ( y ` 0 ) ) -> ( ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) <-> y e. ( N ClWWalksN G ) ) ) |
20 |
15 19
|
rspcedv |
|- ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) -> ( y e. ( N ClWWalksN G ) -> E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) ) ) |
21 |
20
|
adantld |
|- ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) -> ( ( G e. USGraph /\ y e. ( N ClWWalksN G ) ) -> E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) ) ) |
22 |
9 21
|
mpcom |
|- ( ( G e. USGraph /\ y e. ( N ClWWalksN G ) ) -> E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) ) |
23 |
22
|
ex |
|- ( G e. USGraph -> ( y e. ( N ClWWalksN G ) -> E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) ) ) |
24 |
6 23
|
impbid2 |
|- ( G e. USGraph -> ( E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) <-> y e. ( N ClWWalksN G ) ) ) |
25 |
4 24
|
syl5bb |
|- ( G e. USGraph -> ( E. x e. V y e. ( x ( ClWWalksNOn ` G ) N ) <-> y e. ( N ClWWalksN G ) ) ) |
26 |
2 25
|
bitr2id |
|- ( G e. USGraph -> ( y e. ( N ClWWalksN G ) <-> y e. U_ x e. V ( x ( ClWWalksNOn ` G ) N ) ) ) |
27 |
26
|
eqrdv |
|- ( G e. USGraph -> ( N ClWWalksN G ) = U_ x e. V ( x ( ClWWalksNOn ` G ) N ) ) |