upgr1wlkd

Description: In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021)

	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\}$
	upgr1wlkd.g	$⊢ φ \to G \in UPGraph$
Assertion	upgr1wlkd	$⊢ φ \to F Walks (G) P$

Proof

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		upgr1wlkd.g	$⊢ φ \to G \in UPGraph$
7	1 2 3 4 5	upgr1wlkdlem1	$⊢ (φ \land X = Y) \to iEdg (G) (J) = \{X\}$
8	1 2 3 4 5	upgr1wlkdlem2	$⊢ (φ \land X \neq Y) \to \{X, Y\} \subseteq iEdg (G) (J)$
9		eqid	$⊢ Vtx (G) = Vtx (G)$
10		eqid	$⊢ iEdg (G) = iEdg (G)$
11	1 2 3 4 7 8 9 10	1wlkd	$⊢ φ \to F Walks (G) P$

Metamath Proof Explorer

Theorem upgr1wlkd

Proof