upgr1wlkdlem2

	Ref	Expression
Hypotheses	upgr1wlkd.p	$⊢ P = ⟨“ X Y ”⟩$
	upgr1wlkd.f	$⊢ F = ⟨“ J ”⟩$
	upgr1wlkd.x	$⊢ φ \to X \in Vtx (G)$
	upgr1wlkd.y	$⊢ φ \to Y \in Vtx (G)$
	upgr1wlkd.j	$⊢ φ \to iEdg (G) (J) = \{X, Y\}$
Assertion	upgr1wlkdlem2	$⊢ (φ \land X \neq Y) \to \{X, Y\} \subseteq iEdg (G) (J)$

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		ssid	$⊢ \{X, Y\} \subseteq \{X, Y\}$
7		sseq2	$⊢ iEdg (G) (J) = \{X, Y\} \to (\{X, Y\} \subseteq iEdg (G) (J) \leftrightarrow \{X, Y\} \subseteq \{X, Y\})$
8	7	adantl	$⊢ ((φ \land X \neq Y) \land iEdg (G) (J) = \{X, Y\}) \to (\{X, Y\} \subseteq iEdg (G) (J) \leftrightarrow \{X, Y\} \subseteq \{X, Y\})$
9	6 8	mpbiri	$⊢ ((φ \land X \neq Y) \land iEdg (G) (J) = \{X, Y\}) \to \{X, Y\} \subseteq iEdg (G) (J)$
10	5 9	mpidan	$⊢ (φ \land X \neq Y) \to \{X, Y\} \subseteq iEdg (G) (J)$

Metamath Proof Explorer