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∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡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∈WordVtx⁡g|w≠∅∧∀i∈0..^w−1w⁡iw⁡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→WordVtx⁡g=WordV
7 5 6 syl ⊢g=G→WordVtx⁡g=WordV
8 fveq2 ⊢g=G→Edg⁡g=Edg⁡G
9 8 2 eqtr4di ⊢g=G→Edg⁡g=E
10 9 eleq2d ⊢g=G→w⁡iw⁡i+1∈Edg⁡g↔w⁡iw⁡i+1∈E
11 10 ralbidv ⊢g=G→∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g↔∀i∈0..^w−1w⁡iw⁡i+1∈E
12 11 anbi2d ⊢g=G→w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g↔w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E
13 7 12 rabeqbidv ⊢g=G→w∈WordVtx⁡g|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g=w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡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→WordV∈V
18 rabexg ⊢WordV∈V→w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∈V
19 16 17 18 3syl ⊢G∈V→w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∈V
20 3 13 14 19 fvmptd3 ⊢G∈V→WWalks⁡G=w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡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=∅→WordV=Word∅
25 23 24 syl ⊢¬G∈V→WordV=Word∅
26 25 eleq2d ⊢¬G∈V→w∈WordV↔w∈Word∅
27 0wrd0 ⊢w∈Word∅↔w=∅
28 26 27 bitrdi ⊢¬G∈V→w∈WordV↔w=∅
29 nne ⊢¬w≠∅↔w=∅
30 29 biimpri ⊢w=∅→¬w≠∅
31 30 intnanrd ⊢w=∅→¬w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E
32 28 31 syl6bi ⊢¬G∈V→w∈WordV→¬w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E
33 32 ralrimiv ⊢¬G∈V→∀w∈WordV¬w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E
34 rabeq0 ⊢w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E=∅↔∀w∈WordV¬w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E
35 33 34 sylibr ⊢¬G∈V→w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E=∅
36 21 35 eqtr4d ⊢¬G∈V→WWalks⁡G=w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E
37 20 36 pm2.61i ⊢WWalks⁡G=w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E