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 ⊢ G ∈ V ∧ S ∈ ℕ 0 * ∧ I ∈ dom ⁡ iEdg ⁡ G → ⟨“ I ”⟩ ∈ G EdgWalks S

Proof

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