Step |
Hyp |
Ref |
Expression |
0 |
|
cewlks |
|- EdgWalks |
1 |
|
vg |
|- g |
2 |
|
cvv |
|- _V |
3 |
|
vs |
|- s |
4 |
|
cxnn0 |
|- NN0* |
5 |
|
vf |
|- f |
6 |
|
ciedg |
|- iEdg |
7 |
1
|
cv |
|- g |
8 |
7 6
|
cfv |
|- ( iEdg ` g ) |
9 |
|
vi |
|- i |
10 |
5
|
cv |
|- f |
11 |
9
|
cv |
|- i |
12 |
11
|
cdm |
|- dom i |
13 |
12
|
cword |
|- Word dom i |
14 |
10 13
|
wcel |
|- f e. Word dom i |
15 |
|
vk |
|- k |
16 |
|
c1 |
|- 1 |
17 |
|
cfzo |
|- ..^ |
18 |
|
chash |
|- # |
19 |
10 18
|
cfv |
|- ( # ` f ) |
20 |
16 19 17
|
co |
|- ( 1 ..^ ( # ` f ) ) |
21 |
3
|
cv |
|- s |
22 |
|
cle |
|- <_ |
23 |
15
|
cv |
|- k |
24 |
|
cmin |
|- - |
25 |
23 16 24
|
co |
|- ( k - 1 ) |
26 |
25 10
|
cfv |
|- ( f ` ( k - 1 ) ) |
27 |
26 11
|
cfv |
|- ( i ` ( f ` ( k - 1 ) ) ) |
28 |
23 10
|
cfv |
|- ( f ` k ) |
29 |
28 11
|
cfv |
|- ( i ` ( f ` k ) ) |
30 |
27 29
|
cin |
|- ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) |
31 |
30 18
|
cfv |
|- ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) |
32 |
21 31 22
|
wbr |
|- s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) |
33 |
32 15 20
|
wral |
|- A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) |
34 |
14 33
|
wa |
|- ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) |
35 |
34 9 8
|
wsbc |
|- [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) |
36 |
35 5
|
cab |
|- { f | [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) } |
37 |
1 3 2 4 36
|
cmpo |
|- ( g e. _V , s e. NN0* |-> { f | [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) } ) |
38 |
0 37
|
wceq |
|- EdgWalks = ( g e. _V , s e. NN0* |-> { f | [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) } ) |