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

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wwlks.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion iswwlks ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 wwlks.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlks.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 neeq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 ≠ ∅ ↔ 𝑊 ≠ ∅ ) )
4 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) )
5 4 oveq1d ⊢ ( 𝑤 = 𝑊 → ( ( ♯ ‘ 𝑤 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
6 5 oveq2d ⊢ ( 𝑤 = 𝑊 → ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
7 fveq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) )
8 fveq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) )
9 7 8 preq12d ⊢ ( 𝑤 = 𝑊 → { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } )
10 9 eleq1d ⊢ ( 𝑤 = 𝑊 → ( { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
11 6 10 raleqbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
12 3 11 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ↔ ( 𝑊 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
13 12 elrab ⊢ ( 𝑊 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
14 1 2 wwlks ⊢ ( WWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) }
15 14 eleq2i ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ↔ 𝑊 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } )
16 3anan12 ⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
17 13 15 16 3bitr4i ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )