Metamath Proof Explorer


Theorem upgr1pthond

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

Ref Expression
Hypotheses upgr1wlkd.p P = ⟨“ XY ”⟩
upgr1wlkd.f F = ⟨“ J ”⟩
upgr1wlkd.x φ X Vtx G
upgr1wlkd.y φ Y Vtx G
upgr1wlkd.j φ iEdg G J = X Y
upgr1wlkd.g φ G UPGraph
Assertion upgr1pthond φ F X PathsOn G Y P

Proof

Step Hyp Ref Expression
1 upgr1wlkd.p P = ⟨“ XY ”⟩
2 upgr1wlkd.f F = ⟨“ J ”⟩
3 upgr1wlkd.x φ X Vtx G
4 upgr1wlkd.y φ Y Vtx G
5 upgr1wlkd.j φ iEdg G J = X Y
6 upgr1wlkd.g φ G UPGraph
7 1 2 3 4 5 upgr1wlkdlem1 φ X = Y iEdg G J = X
8 1 2 3 4 5 upgr1wlkdlem2 φ X Y X Y iEdg G J
9 eqid Vtx G = Vtx G
10 eqid iEdg G = iEdg G
11 1 2 3 4 7 8 9 10 1pthond φ F X PathsOn G Y P