Theorem wwlksn

Description: The set of walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

	Ref	Expression
Assertion	wwlksn	|- ( N e. NN0 -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( g = G -> ( WWalks ` g ) = ( WWalks ` G ) )
2	1	adantl	|- ( ( n = N /\ g = G ) -> ( WWalks ` g ) = ( WWalks ` G ) )
3		oveq1	|- ( n = N -> ( n + 1 ) = ( N + 1 ) )
4	3	eqeq2d	|- ( n = N -> ( ( # ` w ) = ( n + 1 ) <-> ( # ` w ) = ( N + 1 ) ) )
5	4	adantr	|- ( ( n = N /\ g = G ) -> ( ( # ` w ) = ( n + 1 ) <-> ( # ` w ) = ( N + 1 ) ) )
6	2 5	rabeqbidv	|- ( ( n = N /\ g = G ) -> { w e. ( WWalks ` g ) | ( # ` w ) = ( n + 1 ) } = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } )
7		df-wwlksn	|- WWalksN = ( n e. NN0 , g e. _V |-> { w e. ( WWalks ` g ) | ( # ` w ) = ( n + 1 ) } )
8		fvex	|- ( WWalks ` G ) e. _V
9	8	rabex	|- { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } e. _V
10	6 7 9	ovmpoa	|- ( ( N e. NN0 /\ G e. _V ) -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } )
11	10	expcom	|- ( G e. _V -> ( N e. NN0 -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } ) )
12	7	reldmmpo	|- Rel dom WWalksN
13	12	ovprc2	|- ( -. G e. _V -> ( N WWalksN G ) = (/) )
14		fvprc	|- ( -. G e. _V -> ( WWalks ` G ) = (/) )
15	14	rabeqdv	|- ( -. G e. _V -> { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } = { w e. (/) | ( # ` w ) = ( N + 1 ) } )
16		rab0	|- { w e. (/) | ( # ` w ) = ( N + 1 ) } = (/)
17	15 16	eqtrdi	|- ( -. G e. _V -> { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } = (/) )
18	13 17	eqtr4d	|- ( -. G e. _V -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } )
19	18	a1d	|- ( -. G e. _V -> ( N e. NN0 -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } ) )
20	11 19	pm2.61i	|- ( N e. NN0 -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } )