Metamath Proof Explorer


Theorem upgr1wlkdlem1

Description: Lemma 1 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 upgr1wlkdlem1 φ X = Y iEdg G J = X

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 preq2 Y = X X Y = X X
7 6 eqeq2d Y = X iEdg G J = X Y iEdg G J = X X
8 7 eqcoms X = Y iEdg G J = X Y iEdg G J = X X
9 simpl iEdg G J = X X φ iEdg G J = X X
10 dfsn2 X = X X
11 9 10 eqtr4di iEdg G J = X X φ iEdg G J = X
12 11 ex iEdg G J = X X φ iEdg G J = X
13 8 12 syl6bi X = Y iEdg G J = X Y φ iEdg G J = X
14 13 com13 φ iEdg G J = X Y X = Y iEdg G J = X
15 5 14 mpd φ X = Y iEdg G J = X
16 15 imp φ X = Y iEdg G J = X