Metamath Proof Explorer

Theorem wwlkswwlksn

Description: A walk of a fixed length as word is a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 17-Jul-2018) (Revised by AV, 12-Apr-2021)

Ref Expression
Assertion wwlkswwlksn ⊢ W ∈ N WWalksN G → W ∈ WWalks ⁡ G

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 wwlknbp ⊢ W ∈ N WWalksN G → G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G
3 iswwlksn ⊢ N ∈ ℕ 0 → W ∈ N WWalksN G ↔ W ∈ WWalks ⁡ G ∧ W = N + 1
4 3 3ad2ant2 ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G → W ∈ N WWalksN G ↔ W ∈ WWalks ⁡ G ∧ W = N + 1
5 simpl ⊢ W ∈ WWalks ⁡ G ∧ W = N + 1 → W ∈ WWalks ⁡ G
6 4 5 biimtrdi ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G → W ∈ N WWalksN G → W ∈ WWalks ⁡ G
7 2 6 mpcom ⊢ W ∈ N WWalksN G → W ∈ WWalks ⁡ G