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

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 ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ ( 𝐺 EdgWalks 1 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
2 1 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )
3 1 wlk1walk ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 1 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
4 wlkv ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
5 4 simp1d ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐺 ∈ V )
6 1nn0 ⊢ 1 ∈ ℕ0
7 nn0xnn0 ⊢ ( 1 ∈ ℕ0 → 1 ∈ ℕ0* )
8 6 7 mp1i ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 1 ∈ ℕ0* )
9 1 isewlk ⊢ ( ( 𝐺 ∈ V ∧ 1 ∈ ℕ0* ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 1 ) ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 1 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
10 5 8 2 9 syl3anc ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ ( 𝐺 EdgWalks 1 ) ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 1 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
11 2 3 10 mpbir2and ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ ( 𝐺 EdgWalks 1 ) )