Step |
Hyp |
Ref |
Expression |
0 |
|
cwwspthsnon |
|- WSPathsNOn |
1 |
|
vn |
|- n |
2 |
|
cn0 |
|- NN0 |
3 |
|
vg |
|- g |
4 |
|
cvv |
|- _V |
5 |
|
va |
|- a |
6 |
|
cvtx |
|- Vtx |
7 |
3
|
cv |
|- g |
8 |
7 6
|
cfv |
|- ( Vtx ` g ) |
9 |
|
vb |
|- b |
10 |
|
vw |
|- w |
11 |
5
|
cv |
|- a |
12 |
1
|
cv |
|- n |
13 |
|
cwwlksnon |
|- WWalksNOn |
14 |
12 7 13
|
co |
|- ( n WWalksNOn g ) |
15 |
9
|
cv |
|- b |
16 |
11 15 14
|
co |
|- ( a ( n WWalksNOn g ) b ) |
17 |
|
vf |
|- f |
18 |
17
|
cv |
|- f |
19 |
|
cspthson |
|- SPathsOn |
20 |
7 19
|
cfv |
|- ( SPathsOn ` g ) |
21 |
11 15 20
|
co |
|- ( a ( SPathsOn ` g ) b ) |
22 |
10
|
cv |
|- w |
23 |
18 22 21
|
wbr |
|- f ( a ( SPathsOn ` g ) b ) w |
24 |
23 17
|
wex |
|- E. f f ( a ( SPathsOn ` g ) b ) w |
25 |
24 10 16
|
crab |
|- { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a ( SPathsOn ` g ) b ) w } |
26 |
5 9 8 8 25
|
cmpo |
|- ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a ( SPathsOn ` g ) b ) w } ) |
27 |
1 3 2 4 26
|
cmpo |
|- ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a ( SPathsOn ` g ) b ) w } ) ) |
28 |
0 27
|
wceq |
|- WSPathsNOn = ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a ( SPathsOn ` g ) b ) w } ) ) |