Metamath Proof Explorer


Theorem upgr1wlkdlem2

Description: Lemma 2 for upgr1wlkd . (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
Assertion upgr1wlkdlem2 φ X Y X Y iEdg G J

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 ssid X Y X Y
7 sseq2 iEdg G J = X Y X Y iEdg G J X Y X Y
8 7 adantl φ X Y iEdg G J = X Y X Y iEdg G J X Y X Y
9 6 8 mpbiri φ X Y iEdg G J = X Y X Y iEdg G J
10 5 9 mpidan φ X Y X Y iEdg G J