upgr1wlkdlem1

Step	Hyp	Ref	Expression
1		upgr1wlkd.p	$⊢ P = ⟨“ X Y ”⟩$
2		upgr1wlkd.f	$⊢ F = ⟨“ J ”⟩$
3		upgr1wlkd.x	$⊢ φ \to X \in Vtx (G)$
4		upgr1wlkd.y	$⊢ φ \to Y \in Vtx (G)$
5		upgr1wlkd.j	$⊢ φ \to iEdg (G) (J) = \{X, Y\}$
6		preq2	$⊢ Y = X \to \{X, Y\} = \{X, X\}$
7	6	eqeq2d	$⊢ Y = X \to (iEdg (G) (J) = \{X, Y\} \leftrightarrow iEdg (G) (J) = \{X, X\})$
8	7	eqcoms	$⊢ X = Y \to (iEdg (G) (J) = \{X, Y\} \leftrightarrow iEdg (G) (J) = \{X, X\})$
9		simpl	$⊢ (iEdg (G) (J) = \{X, X\} \land φ) \to iEdg (G) (J) = \{X, X\}$
10		dfsn2	$⊢ \{X\} = \{X, X\}$
11	9 10	eqtr4di	$⊢ (iEdg (G) (J) = \{X, X\} \land φ) \to iEdg (G) (J) = \{X\}$
12	11	ex	$⊢ iEdg (G) (J) = \{X, X\} \to (φ \to iEdg (G) (J) = \{X\})$
13	8 12	syl6bi	$⊢ X = Y \to (iEdg (G) (J) = \{X, Y\} \to (φ \to iEdg (G) (J) = \{X\}))$
14	13	com13	$⊢ φ \to (iEdg (G) (J) = \{X, Y\} \to (X = Y \to iEdg (G) (J) = \{X\}))$
15	5 14	mpd	$⊢ φ \to (X = Y \to iEdg (G) (J) = \{X\})$
16	15	imp	$⊢ (φ \land X = Y) \to iEdg (G) (J) = \{X\}$

Metamath Proof Explorer