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 biimtrdi ⊢ 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