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