Step |
Hyp |
Ref |
Expression |
1 |
|
clwwlkf1o.d |
|- D = { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } |
2 |
|
clwwlkf1o.f |
|- F = ( t e. D |-> ( t prefix N ) ) |
3 |
1 2
|
clwwlkf |
|- ( N e. NN -> F : D --> ( N ClWWalksN G ) ) |
4 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
5 |
|
eqid |
|- ( Edg ` G ) = ( Edg ` G ) |
6 |
4 5
|
clwwlknp |
|- ( p e. ( N ClWWalksN G ) -> ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) ) |
7 |
|
simpr |
|- ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> N e. NN ) |
8 |
|
simpl1 |
|- ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) ) |
9 |
|
3simpc |
|- ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) ) |
10 |
9
|
adantr |
|- ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) ) |
11 |
1
|
clwwlkel |
|- ( ( N e. NN /\ ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) ) -> ( p ++ <" ( p ` 0 ) "> ) e. D ) |
12 |
7 8 10 11
|
syl3anc |
|- ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( p ++ <" ( p ` 0 ) "> ) e. D ) |
13 |
|
oveq2 |
|- ( N = ( # ` p ) -> ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) = ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) ) |
14 |
13
|
eqcoms |
|- ( ( # ` p ) = N -> ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) = ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) ) |
15 |
14
|
adantl |
|- ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) -> ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) = ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) ) |
16 |
15
|
3ad2ant1 |
|- ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) -> ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) = ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) ) |
17 |
16
|
adantr |
|- ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) = ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) ) |
18 |
|
simpll |
|- ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ N e. NN ) -> p e. Word ( Vtx ` G ) ) |
19 |
|
fstwrdne0 |
|- ( ( N e. NN /\ ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) ) -> ( p ` 0 ) e. ( Vtx ` G ) ) |
20 |
19
|
ancoms |
|- ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ N e. NN ) -> ( p ` 0 ) e. ( Vtx ` G ) ) |
21 |
20
|
s1cld |
|- ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ N e. NN ) -> <" ( p ` 0 ) "> e. Word ( Vtx ` G ) ) |
22 |
18 21
|
jca |
|- ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ N e. NN ) -> ( p e. Word ( Vtx ` G ) /\ <" ( p ` 0 ) "> e. Word ( Vtx ` G ) ) ) |
23 |
22
|
3ad2antl1 |
|- ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( p e. Word ( Vtx ` G ) /\ <" ( p ` 0 ) "> e. Word ( Vtx ` G ) ) ) |
24 |
|
pfxccat1 |
|- ( ( p e. Word ( Vtx ` G ) /\ <" ( p ` 0 ) "> e. Word ( Vtx ` G ) ) -> ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) = p ) |
25 |
23 24
|
syl |
|- ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) = p ) |
26 |
17 25
|
eqtr2d |
|- ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> p = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) ) |
27 |
12 26
|
jca |
|- ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( ( p ++ <" ( p ` 0 ) "> ) e. D /\ p = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) ) ) |
28 |
27
|
ex |
|- ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) -> ( N e. NN -> ( ( p ++ <" ( p ` 0 ) "> ) e. D /\ p = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) ) ) ) |
29 |
6 28
|
syl |
|- ( p e. ( N ClWWalksN G ) -> ( N e. NN -> ( ( p ++ <" ( p ` 0 ) "> ) e. D /\ p = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) ) ) ) |
30 |
29
|
impcom |
|- ( ( N e. NN /\ p e. ( N ClWWalksN G ) ) -> ( ( p ++ <" ( p ` 0 ) "> ) e. D /\ p = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) ) ) |
31 |
|
oveq1 |
|- ( x = ( p ++ <" ( p ` 0 ) "> ) -> ( x prefix N ) = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) ) |
32 |
31
|
rspceeqv |
|- ( ( ( p ++ <" ( p ` 0 ) "> ) e. D /\ p = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) ) -> E. x e. D p = ( x prefix N ) ) |
33 |
30 32
|
syl |
|- ( ( N e. NN /\ p e. ( N ClWWalksN G ) ) -> E. x e. D p = ( x prefix N ) ) |
34 |
1 2
|
clwwlkfv |
|- ( x e. D -> ( F ` x ) = ( x prefix N ) ) |
35 |
34
|
eqeq2d |
|- ( x e. D -> ( p = ( F ` x ) <-> p = ( x prefix N ) ) ) |
36 |
35
|
adantl |
|- ( ( ( N e. NN /\ p e. ( N ClWWalksN G ) ) /\ x e. D ) -> ( p = ( F ` x ) <-> p = ( x prefix N ) ) ) |
37 |
36
|
rexbidva |
|- ( ( N e. NN /\ p e. ( N ClWWalksN G ) ) -> ( E. x e. D p = ( F ` x ) <-> E. x e. D p = ( x prefix N ) ) ) |
38 |
33 37
|
mpbird |
|- ( ( N e. NN /\ p e. ( N ClWWalksN G ) ) -> E. x e. D p = ( F ` x ) ) |
39 |
38
|
ralrimiva |
|- ( N e. NN -> A. p e. ( N ClWWalksN G ) E. x e. D p = ( F ` x ) ) |
40 |
|
dffo3 |
|- ( F : D -onto-> ( N ClWWalksN G ) <-> ( F : D --> ( N ClWWalksN G ) /\ A. p e. ( N ClWWalksN G ) E. x e. D p = ( F ` x ) ) ) |
41 |
3 39 40
|
sylanbrc |
|- ( N e. NN -> F : D -onto-> ( N ClWWalksN G ) ) |