Metamath Proof Explorer

Theorem wlk1ewlk

Description: A walk is an s-walk "on the edge level" (with s=1) according to Aksoy et al. (Contributed by AV, 5-Jan-2021)

Ref Expression
Assertion wlk1ewlk ⊢ F Walks ⁡ G P → F ∈ G EdgWalks 1

Proof

Step Hyp Ref Expression
1 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
2 1 wlkf ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ iEdg ⁡ G
3 1 wlk1walk ⊢ F Walks ⁡ G P → ∀ k ∈ 1 ..^ F 1 ≤ iEdg ⁡ G ⁡ F ⁡ k − 1 ∩ iEdg ⁡ G ⁡ F ⁡ k
4 wlkv ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
5 4 simp1d ⊢ F Walks ⁡ G P → G ∈ V
6 1nn0 ⊢ 1 ∈ ℕ 0
7 nn0xnn0 ⊢ 1 ∈ ℕ 0 → 1 ∈ ℕ 0 *
8 6 7 mp1i ⊢ F Walks ⁡ G P → 1 ∈ ℕ 0 *
9 1 isewlk ⊢ G ∈ V ∧ 1 ∈ ℕ 0 * ∧ F ∈ Word dom ⁡ iEdg ⁡ G → F ∈ G EdgWalks 1 ↔ F ∈ Word dom ⁡ iEdg ⁡ G ∧ ∀ k ∈ 1 ..^ F 1 ≤ iEdg ⁡ G ⁡ F ⁡ k − 1 ∩ iEdg ⁡ G ⁡ F ⁡ k
10 5 8 2 9 syl3anc ⊢ F Walks ⁡ G P → F ∈ G EdgWalks 1 ↔ F ∈ Word dom ⁡ iEdg ⁡ G ∧ ∀ k ∈ 1 ..^ F 1 ≤ iEdg ⁡ G ⁡ F ⁡ k − 1 ∩ iEdg ⁡ G ⁡ F ⁡ k
11 2 3 10 mpbir2and ⊢ F Walks ⁡ G P → F ∈ G EdgWalks 1