1pthd

Description: In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Revised by AV, 22-Jan-2021) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Hypotheses	1wlkd.p	$⊢ P = ⟨“ X Y ”⟩$
	1wlkd.f	$⊢ F = ⟨“ J ”⟩$
	1wlkd.x	$⊢ φ \to X \in V$
	1wlkd.y	$⊢ φ \to Y \in V$
	1wlkd.l	$⊢ (φ \land X = Y) \to I (J) = \{X\}$
	1wlkd.j	$⊢ (φ \land X \neq Y) \to \{X, Y\} \subseteq I (J)$
	1wlkd.v	$⊢ V = Vtx (G)$
	1wlkd.i	$⊢ I = iEdg (G)$
Assertion	1pthd	$⊢ φ \to F Paths (G) P$

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	$⊢ P = ⟨“ X Y ”⟩$
2		1wlkd.f	$⊢ F = ⟨“ J ”⟩$
3		1wlkd.x	$⊢ φ \to X \in V$
4		1wlkd.y	$⊢ φ \to Y \in V$
5		1wlkd.l	$⊢ (φ \land X = Y) \to I (J) = \{X\}$
6		1wlkd.j	$⊢ (φ \land X \neq Y) \to \{X, Y\} \subseteq I (J)$
7		1wlkd.v	$⊢ V = Vtx (G)$
8		1wlkd.i	$⊢ I = iEdg (G)$
9	1 2 3 4 5 6 7 8	1trld	$⊢ φ \to F Trails (G) P$
10		simpr	$⊢ (φ \land F Trails (G) P) \to F Trails (G) P$
11	1 2	1pthdlem1	$⊢ Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}$
12	11	a1i	$⊢ (φ \land F Trails (G) P) \to Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}$
13	1 2	1pthdlem2	$⊢ P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset$
14	13	a1i	$⊢ (φ \land F Trails (G) P) \to P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset$
15		ispth	$⊢ F Paths (G) P \leftrightarrow (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)$
16	10 12 14 15	syl3anbrc	$⊢ (φ \land F Trails (G) P) \to F Paths (G) P$
17	9 16	mpdan	$⊢ φ \to F Paths (G) P$

Metamath Proof Explorer

Theorem 1pthd

Proof