Metamath Proof Explorer


Theorem clwwlkfv

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 N WWalksN G | lastS w = w 0
clwwlkf1o.f F = t D t prefix N
Assertion clwwlkfv W D F W = W prefix N

Proof

Step Hyp Ref Expression
1 clwwlkf1o.d D = w N WWalksN G | lastS w = w 0
2 clwwlkf1o.f F = t D t prefix N
3 oveq1 t = W t prefix N = W prefix N
4 ovex W prefix N V
5 3 2 4 fvmpt W D F W = W prefix N