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 𝑉 = ( Vtx ‘ 𝐺 )
wwlks.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion wwlks ( WWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) }

Proof

Step Hyp Ref Expression
1 wwlks.v 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlks.e 𝐸 = ( Edg ‘ 𝐺 )
3 df-wwlks WWalks = ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ) } )
4 fveq2 ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
5 4 1 eqtr4di ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
6 wrdeq ( ( Vtx ‘ 𝑔 ) = 𝑉 → Word ( Vtx ‘ 𝑔 ) = Word 𝑉 )
7 5 6 syl ( 𝑔 = 𝐺 → Word ( Vtx ‘ 𝑔 ) = Word 𝑉 )
8 fveq2 ( 𝑔 = 𝐺 → ( Edg ‘ 𝑔 ) = ( Edg ‘ 𝐺 ) )
9 8 2 eqtr4di ( 𝑔 = 𝐺 → ( Edg ‘ 𝑔 ) = 𝐸 )
10 9 eleq2d ( 𝑔 = 𝐺 → ( { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ↔ { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
11 10 ralbidv ( 𝑔 = 𝐺 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
12 11 anbi2d ( 𝑔 = 𝐺 → ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ) ↔ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
13 7 12 rabeqbidv ( 𝑔 = 𝐺 → { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ) } = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } )
14 id ( 𝐺 ∈ V → 𝐺 ∈ V )
15 1 fvexi 𝑉 ∈ V
16 15 a1i ( 𝐺 ∈ V → 𝑉 ∈ V )
17 wrdexg ( 𝑉 ∈ V → Word 𝑉 ∈ V )
18 rabexg ( Word 𝑉 ∈ V → { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } ∈ V )
19 16 17 18 3syl ( 𝐺 ∈ V → { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } ∈ V )
20 3 13 14 19 fvmptd3 ( 𝐺 ∈ V → ( WWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } )
21 fvprc ( ¬ 𝐺 ∈ V → ( WWalks ‘ 𝐺 ) = ∅ )
22 fvprc ( ¬ 𝐺 ∈ V → ( Vtx ‘ 𝐺 ) = ∅ )
23 1 22 syl5eq ( ¬ 𝐺 ∈ V → 𝑉 = ∅ )
24 wrdeq ( 𝑉 = ∅ → Word 𝑉 = Word ∅ )
25 23 24 syl ( ¬ 𝐺 ∈ V → Word 𝑉 = Word ∅ )
26 25 eleq2d ( ¬ 𝐺 ∈ V → ( 𝑤 ∈ Word 𝑉𝑤 ∈ Word ∅ ) )
27 0wrd0 ( 𝑤 ∈ Word ∅ ↔ 𝑤 = ∅ )
28 26 27 bitrdi ( ¬ 𝐺 ∈ V → ( 𝑤 ∈ Word 𝑉𝑤 = ∅ ) )
29 nne ( ¬ 𝑤 ≠ ∅ ↔ 𝑤 = ∅ )
30 29 biimpri ( 𝑤 = ∅ → ¬ 𝑤 ≠ ∅ )
31 30 intnanrd ( 𝑤 = ∅ → ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
32 28 31 syl6bi ( ¬ 𝐺 ∈ V → ( 𝑤 ∈ Word 𝑉 → ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
33 32 ralrimiv ( ¬ 𝐺 ∈ V → ∀ 𝑤 ∈ Word 𝑉 ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
34 rabeq0 ( { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } = ∅ ↔ ∀ 𝑤 ∈ Word 𝑉 ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
35 33 34 sylibr ( ¬ 𝐺 ∈ V → { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } = ∅ )
36 21 35 eqtr4d ( ¬ 𝐺 ∈ V → ( WWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } )
37 20 36 pm2.61i ( WWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) }