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 φXVtxG
upgr1wlkd.y φYVtxG
upgr1wlkd.j φiEdgGJ=XY
Assertion upgr1wlkdlem2 φXYXYiEdgGJ

Proof

Step Hyp Ref Expression
1 upgr1wlkd.p P=⟨“XY”⟩
2 upgr1wlkd.f F=⟨“J”⟩
3 upgr1wlkd.x φXVtxG
4 upgr1wlkd.y φYVtxG
5 upgr1wlkd.j φiEdgGJ=XY
6 ssid XYXY
7 sseq2 iEdgGJ=XYXYiEdgGJXYXY
8 7 adantl φXYiEdgGJ=XYXYiEdgGJXYXY
9 6 8 mpbiri φXYiEdgGJ=XYXYiEdgGJ
10 5 9 mpidan φXYXYiEdgGJ