This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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