Metamath Proof Explorer

Theorem wwlknbp1

Description: Other basic properties of a walk of a fixed length as word. (Contributed by AV, 8-Mar-2022)

Ref Expression
Assertion wwlknbp1 ⊢ W ∈ N WWalksN G → N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1

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 eqid ⊢ Edg ⁡ G = Edg ⁡ G
4 1 3 wwlknp ⊢ W ∈ N WWalksN G → W ∈ Word Vtx ⁡ G ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G
5 simpl ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G → N ∈ ℕ 0
6 simpr1 ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G → W ∈ Word Vtx ⁡ G
7 simpr2 ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G → W = N + 1
8 5 6 7 3jca ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G → N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1
9 8 ex ⊢ N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G → N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1
10 9 3ad2ant2 ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G → W ∈ Word Vtx ⁡ G ∧ W = N + 1 ∧ ∀ i ∈ 0 ..^ N W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G → N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1
11 2 4 10 sylc ⊢ W ∈ N WWalksN G → N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1