Metamath Proof Explorer


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