Metamath Proof Explorer

Theorem wwlks

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

Ref Expression
Hypotheses wwlks.v 
|- V = ( Vtx ` G )
wwlks.e 
|- E = ( Edg ` G )
Assertion wwlks 
|- ( WWalks ` G ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) }

Proof

Step Hyp Ref Expression
1 wwlks.v 
 |-  V = ( Vtx ` G )
2 wwlks.e 
 |-  E = ( Edg ` G )
3 df-wwlks 
 |-  WWalks = ( g e. _V |-> { w e. Word ( Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) ) } )
4 fveq2 
 |-  ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
5 4 1 eqtr4di 
 |-  ( g = G -> ( Vtx ` g ) = V )
6 wrdeq 
 |-  ( ( Vtx ` g ) = V -> Word ( Vtx ` g ) = Word V )
7 5 6 syl 
 |-  ( g = G -> Word ( Vtx ` g ) = Word V )
8 fveq2 
 |-  ( g = G -> ( Edg ` g ) = ( Edg ` G ) )
9 8 2 eqtr4di 
 |-  ( g = G -> ( Edg ` g ) = E )
10 9 eleq2d 
 |-  ( g = G -> ( { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) <-> { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) )
11 10 ralbidv 
 |-  ( g = G -> ( A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) <-> A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) )
12 11 anbi2d 
 |-  ( g = G -> ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) ) <-> ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) ) )
13 7 12 rabeqbidv 
 |-  ( g = G -> { w e. Word ( Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) ) } = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) } )
14 id 
 |-  ( G e. _V -> G e. _V )
15 1 fvexi 
 |-  V e. _V
16 15 a1i 
 |-  ( G e. _V -> V e. _V )
17 wrdexg 
 |-  ( V e. _V -> Word V e. _V )
18 rabexg 
 |-  ( Word V e. _V -> { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) } e. _V )
19 16 17 18 3syl 
 |-  ( G e. _V -> { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) } e. _V )
20 3 13 14 19 fvmptd3 
 |-  ( G e. _V -> ( WWalks ` G ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) } )
21 fvprc 
 |-  ( -. G e. _V -> ( WWalks ` G ) = (/) )
22 fvprc 
 |-  ( -. G e. _V -> ( Vtx ` G ) = (/) )
23 1 22 eqtrid 
 |-  ( -. G e. _V -> V = (/) )
24 wrdeq 
 |-  ( V = (/) -> Word V = Word (/) )
25 23 24 syl 
 |-  ( -. G e. _V -> Word V = Word (/) )
26 25 eleq2d 
 |-  ( -. G e. _V -> ( w e. Word V <-> w e. Word (/) ) )
27 0wrd0 
 |-  ( w e. Word (/) <-> w = (/) )
28 26 27 bitrdi 
 |-  ( -. G e. _V -> ( w e. Word V <-> w = (/) ) )
29 nne 
 |-  ( -. w =/= (/) <-> w = (/) )
30 29 biimpri 
 |-  ( w = (/) -> -. w =/= (/) )
31 30 intnanrd 
 |-  ( w = (/) -> -. ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) )
32 28 31 syl6bi 
 |-  ( -. G e. _V -> ( w e. Word V -> -. ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) ) )
33 32 ralrimiv 
 |-  ( -. G e. _V -> A. w e. Word V -. ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) )
34 rabeq0 
 |-  ( { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) } = (/) <-> A. w e. Word V -. ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) )
35 33 34 sylibr 
 |-  ( -. G e. _V -> { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) } = (/) )
36 21 35 eqtr4d 
 |-  ( -. G e. _V -> ( WWalks ` G ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) } )
37 20 36 pm2.61i 
 |-  ( WWalks ` G ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) }