Metamath Proof Explorer

Theorem clwwlk

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

Ref Expression
Hypotheses clwwlk.v ⊢V=Vtx⁡G
clwwlk.e ⊢E=Edg⁡G
Assertion clwwlk ⊢ClWWalks⁡G=w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E

Proof

Step Hyp Ref Expression
1 clwwlk.v ⊢V=Vtx⁡G
2 clwwlk.e ⊢E=Edg⁡G
3 df-clwwlk ⊢ClWWalks=g∈V⟼w∈WordVtx⁡g|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g∧lastS⁡ww⁡0∈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 9 eleq2d ⊢g=G→lastS⁡ww⁡0∈Edg⁡g↔lastS⁡ww⁡0∈E
13 11 12 3anbi23d ⊢g=G→w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g∧lastS⁡ww⁡0∈Edg⁡g↔w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E
14 7 13 rabeqbidv ⊢g=G→w∈WordVtx⁡g|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g∧lastS⁡ww⁡0∈Edg⁡g=w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E
15 id ⊢G∈V→G∈V
16 1 fvexi ⊢V∈V
17 16 a1i ⊢G∈V→V∈V
18 wrdexg ⊢V∈V→WordV∈V
19 rabexg ⊢WordV∈V→w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E∈V
20 17 18 19 3syl ⊢G∈V→w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E∈V
21 3 14 15 20 fvmptd3 ⊢G∈V→ClWWalks⁡G=w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E
22 fvprc ⊢¬G∈V→ClWWalks⁡G=∅
23 noel ⊢¬lastS⁡ww⁡0∈∅
24 fvprc ⊢¬G∈V→Edg⁡G=∅
25 2 24 eqtrid ⊢¬G∈V→E=∅
26 25 eleq2d ⊢¬G∈V→lastS⁡ww⁡0∈E↔lastS⁡ww⁡0∈∅
27 23 26 mtbiri ⊢¬G∈V→¬lastS⁡ww⁡0∈E
28 27 adantr ⊢¬G∈V∧w∈WordV→¬lastS⁡ww⁡0∈E
29 28 intn3an3d ⊢¬G∈V∧w∈WordV→¬w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E
30 29 ralrimiva ⊢¬G∈V→∀w∈WordV¬w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E
31 rabeq0 ⊢w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E=∅↔∀w∈WordV¬w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E
32 30 31 sylibr ⊢¬G∈V→w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E=∅
33 22 32 eqtr4d ⊢¬G∈V→ClWWalks⁡G=w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E
34 21 33 pm2.61i ⊢ClWWalks⁡G=w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E