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=\left\{w\in \left(N\mathrm{WWalksN}G\right)|\mathrm{lastS}\left(w\right)=w\left(0\right)\right\}$$
	clwwlkf1o.f	$$⊢F=\left(t\in D⟼t\mathrm{prefix}N\right)$$
Assertion	clwwlkfv	$$⊢W\in D\to F\left(W\right)=W\mathrm{prefix}N$$

Proof

Step	Hyp	Ref	Expression
1		clwwlkf1o.d	$$⊢D=\left\{w\in \left(N\mathrm{WWalksN}G\right)|\mathrm{lastS}\left(w\right)=w\left(0\right)\right\}$$
2		clwwlkf1o.f	$$⊢F=\left(t\in D⟼t\mathrm{prefix}N\right)$$
3		oveq1	$$⊢t=W\to t\mathrm{prefix}N=W\mathrm{prefix}N$$
4		ovex	$$⊢W\mathrm{prefix}N\in \mathrm{V}$$
5	3 2 4	fvmpt	$$⊢W\in D\to F\left(W\right)=W\mathrm{prefix}N$$