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

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 eqtrid ⊢ ( ¬ 𝐺 ∈ 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 biimtrdi ⊢ ( ¬ 𝐺 ∈ 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 ) ) } ∈ 𝐸 ) }