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 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 ) )

Proof

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 ) )