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	⊢ 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
	clwwlkf1o.f	⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝑡 prefix 𝑁 ) )
Assertion	clwwlkfv	⊢ ( 𝑊 ∈ 𝐷 → ( 𝐹 ‘ 𝑊 ) = ( 𝑊 prefix 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		clwwlkf1o.d	⊢ 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
2		clwwlkf1o.f	⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝑡 prefix 𝑁 ) )
3		oveq1	⊢ ( 𝑡 = 𝑊 → ( 𝑡 prefix 𝑁 ) = ( 𝑊 prefix 𝑁 ) )
4		ovex	⊢ ( 𝑊 prefix 𝑁 ) ∈ V
5	3 2 4	fvmpt	⊢ ( 𝑊 ∈ 𝐷 → ( 𝐹 ‘ 𝑊 ) = ( 𝑊 prefix 𝑁 ) )