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

Metamath Proof Explorer

Theorem iswwlksn

Description: A word over the set of vertices representing a walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

Ref Expression
Assertion iswwlksn ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 wwlksn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } )
2 1 eleq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ 𝑊 ∈ { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ) )
3 fveqeq2 ⊢ ( 𝑤 = 𝑊 → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) )
4 3 elrab ⊢ ( 𝑊 ∈ { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) )
5 2 4 bitrdi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) )