Description: Lemma 2 for clwwlkf1o : the value of function F. (Contributed by Alexander van der Vekens, 28-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 1-Nov-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | clwwlkf1o.d | |- D = { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } |
|
| clwwlkf1o.f | |- F = ( t e. D |-> ( t prefix N ) ) |
||
| Assertion | clwwlkfv | |- ( W e. D -> ( F ` W ) = ( W prefix N ) ) |
| 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 | oveq1 | |- ( t = W -> ( t prefix N ) = ( W prefix N ) ) |
|
| 4 | ovex | |- ( W prefix N ) e. _V |
|
| 5 | 3 2 4 | fvmpt | |- ( W e. D -> ( F ` W ) = ( W prefix N ) ) |