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 ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E

Proof

Step Hyp Ref Expression
1 wwlks.v ⊢ V = Vtx ⁡ G
2 wwlks.e ⊢ E = Edg ⁡ G
3 df-wwlks ⊢ WWalks = g ∈ V ⟼ w ∈ Word Vtx ⁡ g | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ 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 ∈ Edg ⁡ g ↔ w ⁡ i w ⁡ i + 1 ∈ E
11 10 ralbidv ⊢ g = G → ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g ↔ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E
12 11 anbi2d ⊢ g = G → w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g ↔ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E
13 7 12 rabeqbidv ⊢ g = G → w ∈ Word Vtx ⁡ g | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g = w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E
14 id ⊢ G ∈ V → G ∈ V
15 1 fvexi ⊢ V ∈ V
16 15 a1i ⊢ G ∈ V → V ∈ V
17 wrdexg ⊢ V ∈ V → Word V ∈ V
18 rabexg ⊢ Word V ∈ V → w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∈ V
19 16 17 18 3syl ⊢ G ∈ V → w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∈ V
20 3 13 14 19 fvmptd3 ⊢ G ∈ V → WWalks ⁡ G = w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E
21 fvprc ⊢ ¬ G ∈ V → WWalks ⁡ G = ∅
22 fvprc ⊢ ¬ G ∈ V → Vtx ⁡ G = ∅
23 1 22 eqtrid ⊢ ¬ G ∈ V → V = ∅
24 wrdeq ⊢ V = ∅ → Word V = Word ∅
25 23 24 syl ⊢ ¬ G ∈ V → Word V = Word ∅
26 25 eleq2d ⊢ ¬ G ∈ V → w ∈ Word V ↔ w ∈ Word ∅
27 0wrd0 ⊢ w ∈ Word ∅ ↔ w = ∅
28 26 27 bitrdi ⊢ ¬ G ∈ V → w ∈ Word V ↔ w = ∅
29 nne ⊢ ¬ w ≠ ∅ ↔ w = ∅
30 29 biimpri ⊢ w = ∅ → ¬ w ≠ ∅
31 30 intnanrd ⊢ w = ∅ → ¬ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E
32 28 31 syl6bi ⊢ ¬ G ∈ V → w ∈ Word V → ¬ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E
33 32 ralrimiv ⊢ ¬ G ∈ V → ∀ w ∈ Word V ¬ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E
34 rabeq0 ⊢ w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E = ∅ ↔ ∀ w ∈ Word V ¬ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E
35 33 34 sylibr ⊢ ¬ G ∈ V → w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E = ∅
36 21 35 eqtr4d ⊢ ¬ G ∈ V → WWalks ⁡ G = w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E
37 20 36 pm2.61i ⊢ WWalks ⁡ G = w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E