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 ⊢ N ∈ ℕ 0 → W ∈ N WWalksN G ↔ W ∈ WWalks ⁡ G ∧ W = N + 1

Proof

Step Hyp Ref Expression
1 wwlksn ⊢ N ∈ ℕ 0 → N WWalksN G = w ∈ WWalks ⁡ G | w = N + 1
2 1 eleq2d ⊢ N ∈ ℕ 0 → W ∈ N WWalksN G ↔ W ∈ w ∈ WWalks ⁡ G | w = N + 1
3 fveqeq2 ⊢ w = W → w = N + 1 ↔ W = N + 1
4 3 elrab ⊢ W ∈ w ∈ WWalks ⁡ G | w = N + 1 ↔ W ∈ WWalks ⁡ G ∧ W = N + 1
5 2 4 bitrdi ⊢ N ∈ ℕ 0 → W ∈ N WWalksN G ↔ W ∈ WWalks ⁡ G ∧ W = N + 1