Metamath Proof Explorer

Theorem 1wlkd

Description: In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021) (Revised by AV, 23-Mar-2021)

Ref Expression
Hypotheses 1wlkd.p ⊢ P = ⟨“ XY ”⟩
1wlkd.f ⊢ F = ⟨“ J ”⟩
1wlkd.x ⊢ φ → X ∈ V
1wlkd.y ⊢ φ → Y ∈ V
1wlkd.l ⊢ φ ∧ X = Y → I ⁡ J = X
1wlkd.j ⊢ φ ∧ X ≠ Y → X Y ⊆ I ⁡ J
1wlkd.v ⊢ V = Vtx ⁡ G
1wlkd.i ⊢ I = iEdg ⁡ G
Assertion 1wlkd ⊢ φ → F Walks ⁡ G P

Proof

Step Hyp Ref Expression
1 1wlkd.p ⊢ P = ⟨“ XY ”⟩
2 1wlkd.f ⊢ F = ⟨“ J ”⟩
3 1wlkd.x ⊢ φ → X ∈ V
4 1wlkd.y ⊢ φ → Y ∈ V
5 1wlkd.l ⊢ φ ∧ X = Y → I ⁡ J = X
6 1wlkd.j ⊢ φ ∧ X ≠ Y → X Y ⊆ I ⁡ J
7 1wlkd.v ⊢ V = Vtx ⁡ G
8 1wlkd.i ⊢ I = iEdg ⁡ G
9 1 2 3 4 5 6 1wlkdlem3 ⊢ φ → F ∈ Word dom ⁡ I
10 1 2 3 4 1wlkdlem1 ⊢ φ → P : 0 … F ⟶ V
11 1 2 3 4 5 6 1wlkdlem4 ⊢ φ → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
12 7 1vgrex ⊢ X ∈ V → G ∈ V
13 7 8 iswlkg ⊢ G ∈ V → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
14 3 12 13 3syl ⊢ φ → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
15 9 10 11 14 mpbir3and ⊢ φ → F Walks ⁡ G P