Metamath Proof Explorer

Theorem 1ewlk

Description: A sequence of 1 edge is an s-walk of edges for all s. (Contributed by AV, 5-Jan-2021)

Ref Expression
Assertion 1ewlk ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ∧ 𝐼 ∈ dom ( iEdg ‘ 𝐺 ) ) → ⟨“ 𝐼 ”⟩ ∈ ( 𝐺 EdgWalks 𝑆 ) )

Proof

Step Hyp Ref Expression
1 s1cl ⊢ ( 𝐼 ∈ dom ( iEdg ‘ 𝐺 ) → ⟨“ 𝐼 ”⟩ ∈ Word dom ( iEdg ‘ 𝐺 ) )
2 1 3ad2ant3 ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ∧ 𝐼 ∈ dom ( iEdg ‘ 𝐺 ) ) → ⟨“ 𝐼 ”⟩ ∈ Word dom ( iEdg ‘ 𝐺 ) )
3 ral0 ⊢ ∀ 𝑘 ∈ ∅ 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ 𝑘 ) ) ) )
4 s1len ⊢ ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) = 1
5 4 oveq2i ⊢ ( 1 ..^ ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) = ( 1 ..^ 1 )
6 fzo0 ⊢ ( 1 ..^ 1 ) = ∅
7 5 6 eqtri ⊢ ( 1 ..^ ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) = ∅
8 7 a1i ⊢ ( 𝐼 ∈ dom ( iEdg ‘ 𝐺 ) → ( 1 ..^ ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) = ∅ )
9 8 raleqdv ⊢ ( 𝐼 ∈ dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ 𝑘 ) ) ) ) ↔ ∀ 𝑘 ∈ ∅ 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ 𝑘 ) ) ) ) ) )
10 3 9 mpbiri ⊢ ( 𝐼 ∈ dom ( iEdg ‘ 𝐺 ) → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ 𝑘 ) ) ) ) )
11 10 3ad2ant3 ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ∧ 𝐼 ∈ dom ( iEdg ‘ 𝐺 ) ) → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ 𝑘 ) ) ) ) )
12 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
13 12 isewlk ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ∧ ⟨“ 𝐼 ”⟩ ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ⟨“ 𝐼 ”⟩ ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ ( ⟨“ 𝐼 ”⟩ ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ 𝑘 ) ) ) ) ) ) )
14 1 13 syl3an3 ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ∧ 𝐼 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ⟨“ 𝐼 ”⟩ ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ ( ⟨“ 𝐼 ”⟩ ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ⟨“ 𝐼 ”⟩ ‘ 𝑘 ) ) ) ) ) ) )
15 2 11 14 mpbir2and ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ∧ 𝐼 ∈ dom ( iEdg ‘ 𝐺 ) ) → ⟨“ 𝐼 ”⟩ ∈ ( 𝐺 EdgWalks 𝑆 ) )