Metamath Proof Explorer

Theorem iswwlks

Description: A word over the set of vertices representing a walk (in an undirected graph). (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 iswwlks ⊢W∈WWalks⁡G↔W≠∅∧W∈WordV∧∀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 neeq1 ⊢w=W→w≠∅↔W≠∅
4 fveq2 ⊢w=W→w=W
5 4 oveq1d ⊢w=W→w−1=W−1
6 5 oveq2d ⊢w=W→0..^w−1=0..^W−1
7 fveq1 ⊢w=W→w⁡i=W⁡i
8 fveq1 ⊢w=W→w⁡i+1=W⁡i+1
9 7 8 preq12d ⊢w=W→w⁡iw⁡i+1=W⁡iW⁡i+1
10 9 eleq1d ⊢w=W→w⁡iw⁡i+1∈E↔W⁡iW⁡i+1∈E
11 6 10 raleqbidv ⊢w=W→∀i∈0..^w−1w⁡iw⁡i+1∈E↔∀i∈0..^W−1W⁡iW⁡i+1∈E
12 3 11 anbi12d ⊢w=W→w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E↔W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E
13 12 elrab ⊢W∈w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E
14 1 2 wwlks ⊢WWalks⁡G=w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E
15 14 eleq2i ⊢W∈WWalks⁡G↔W∈w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E
16 3anan12 ⊢W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E
17 13 15 16 3bitr4i ⊢W∈WWalks⁡G↔W≠∅∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E