Description: The restriction <. H , Q >. of a trail <. F , P >. to an initial segment of the trail (of length N ) forms a trail on the subgraph S consisting of the edges in the initial segment. (Contributed by AV, 6-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | trlres.v | |
|
trlres.i | |
||
trlres.d | |
||
trlres.n | |
||
trlres.h | |
||
trlres.s | |
||
trlres.e | |
||
trlres.q | |
||
Assertion | trlres | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | trlres.v | |
|
2 | trlres.i | |
|
3 | trlres.d | |
|
4 | trlres.n | |
|
5 | trlres.h | |
|
6 | trlres.s | |
|
7 | trlres.e | |
|
8 | trlres.q | |
|
9 | trliswlk | |
|
10 | 3 9 | syl | |
11 | 1 2 10 4 6 7 5 8 | wlkres | |
12 | 1 2 3 4 5 | trlreslem | |
13 | f1of1 | |
|
14 | df-f1 | |
|
15 | 14 | simprbi | |
16 | 12 13 15 | 3syl | |
17 | istrl | |
|
18 | 11 16 17 | sylanbrc | |