Metamath Proof Explorer

Theorem numclwlk2lem2fv

Description: Value of the function R . (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 31-May-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses numclwwlk.v 
|- V = ( Vtx ` G )
numclwwlk.q 
|- Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
numclwwlk.h 
|- H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
numclwwlk.r 
|- R = ( x e. ( X H ( N + 2 ) ) |-> ( x prefix ( N + 1 ) ) )
Assertion numclwlk2lem2fv 
|- ( ( X e. V /\ N e. NN ) -> ( W e. ( X H ( N + 2 ) ) -> ( R ` W ) = ( W prefix ( N + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 numclwwlk.v 
 |-  V = ( Vtx ` G )
2 numclwwlk.q 
 |-  Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
3 numclwwlk.h 
 |-  H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
4 numclwwlk.r 
 |-  R = ( x e. ( X H ( N + 2 ) ) |-> ( x prefix ( N + 1 ) ) )
5 oveq1 
 |-  ( x = W -> ( x prefix ( N + 1 ) ) = ( W prefix ( N + 1 ) ) )
6 simpr 
 |-  ( ( ( X e. V /\ N e. NN ) /\ W e. ( X H ( N + 2 ) ) ) -> W e. ( X H ( N + 2 ) ) )
7 ovexd 
 |-  ( ( ( X e. V /\ N e. NN ) /\ W e. ( X H ( N + 2 ) ) ) -> ( W prefix ( N + 1 ) ) e. _V )
8 4 5 6 7 fvmptd3 
 |-  ( ( ( X e. V /\ N e. NN ) /\ W e. ( X H ( N + 2 ) ) ) -> ( R ` W ) = ( W prefix ( N + 1 ) ) )
9 8 ex 
 |-  ( ( X e. V /\ N e. NN ) -> ( W e. ( X H ( N + 2 ) ) -> ( R ` W ) = ( W prefix ( N + 1 ) ) ) )