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 𝐷 = { 𝑤 ∈ ( 𝑁 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 𝑁 ) )