Theorem wwlksnexthasheq

Description: The number of the extensions of a walk (as word) by an edge equals the number of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 23-Aug-2018) (Revised by AV, 19-Apr-2021) (Revised by AV, 27-Oct-2022)

	Ref	Expression
Hypotheses	wwlksnexthasheq.v	|- V = ( Vtx ` G )
	wwlksnexthasheq.e	|- E = ( Edg ` G )
Assertion	wwlksnexthasheq	|- ( W e. ( N WWalksN G ) -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } ) = ( # ` { n e. V | { ( lastS ` W ) , n } e. E } ) )

Proof

Step	Hyp	Ref	Expression
1		wwlksnexthasheq.v	|- V = ( Vtx ` G )
2		wwlksnexthasheq.e	|- E = ( Edg ` G )
3		ovex	|- ( ( N + 1 ) WWalksN G ) e. _V
4	3	rabex	|- { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } e. _V
5	1 2	wwlksnextbij	|- ( W e. ( N WWalksN G ) -> E. f f : { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } -1-1-onto-> { n e. V | { ( lastS ` W ) , n } e. E } )
6		hasheqf1oi	|- ( { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } e. _V -> ( E. f f : { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } -1-1-onto-> { n e. V | { ( lastS ` W ) , n } e. E } -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } ) = ( # ` { n e. V | { ( lastS ` W ) , n } e. E } ) ) )
7	4 5 6	mpsyl	|- ( W e. ( N WWalksN G ) -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } ) = ( # ` { n e. V | { ( lastS ` W ) , n } e. E } ) )