1pthond

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 from one of these vertices to the other vertex. 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, 4-Dec-2017) (Revised by AV, 22-Jan-2021) (Revised by AV, 23-Mar-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	1pthond	$⊢ φ \to F (X PathsOn (G) Y) 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	1wlkd	$⊢ φ \to F Walks (G) P$
10	1	fveq1i	$⊢ P (0) = ⟨“ X Y ”⟩ (0)$
11		s2fv0	$⊢ X \in V \to ⟨“ X Y ”⟩ (0) = X$
12	10 11	syl5eq	$⊢ X \in V \to P (0) = X$
13	3 12	syl	$⊢ φ \to P (0) = X$
14	2	fveq2i	$⊢ \|F\| = \|⟨“ J ”⟩\|$
15		s1len	$⊢ \|⟨“ J ”⟩\| = 1$
16	14 15	eqtri	$⊢ \|F\| = 1$
17	1 16	fveq12i	$⊢ P (\|F\|) = ⟨“ X Y ”⟩ (1)$
18		s2fv1	$⊢ Y \in V \to ⟨“ X Y ”⟩ (1) = Y$
19	4 18	syl	$⊢ φ \to ⟨“ X Y ”⟩ (1) = Y$
20	17 19	syl5eq	$⊢ φ \to P (\|F\|) = Y$
21		wlkv	$⊢ F Walks (G) P \to (G \in V \land F \in V \land P \in V)$
22		3simpc	$⊢ (G \in V \land F \in V \land P \in V) \to (F \in V \land P \in V)$
23	9 21 22	3syl	$⊢ φ \to (F \in V \land P \in V)$
24	3 4 23	jca31	$⊢ φ \to ((X \in V \land Y \in V) \land (F \in V \land P \in V))$
25	7	iswlkon	$⊢ ((X \in V \land Y \in V) \land (F \in V \land P \in V)) \to (F (X WalksOn (G) Y) P \leftrightarrow (F Walks (G) P \land P (0) = X \land P (\|F\|) = Y))$
26	24 25	syl	$⊢ φ \to (F (X WalksOn (G) Y) P \leftrightarrow (F Walks (G) P \land P (0) = X \land P (\|F\|) = Y))$
27	9 13 20 26	mpbir3and	$⊢ φ \to F (X WalksOn (G) Y) P$
28	1 2 3 4 5 6 7 8	1trld	$⊢ φ \to F Trails (G) P$
29	7	istrlson	$⊢ ((X \in V \land Y \in V) \land (F \in V \land P \in V)) \to (F (X TrailsOn (G) Y) P \leftrightarrow (F (X WalksOn (G) Y) P \land F Trails (G) P))$
30	24 29	syl	$⊢ φ \to (F (X TrailsOn (G) Y) P \leftrightarrow (F (X WalksOn (G) Y) P \land F Trails (G) P))$
31	27 28 30	mpbir2and	$⊢ φ \to F (X TrailsOn (G) Y) P$
32	1 2 3 4 5 6 7 8	1pthd	$⊢ φ \to F Paths (G) P$
33	3	adantl	$⊢ ((F \in V \land P \in V) \land φ) \to X \in V$
34	4	adantl	$⊢ ((F \in V \land P \in V) \land φ) \to Y \in V$
35		simpl	$⊢ ((F \in V \land P \in V) \land φ) \to (F \in V \land P \in V)$
36	33 34 35	jca31	$⊢ ((F \in V \land P \in V) \land φ) \to ((X \in V \land Y \in V) \land (F \in V \land P \in V))$
37	36	ex	$⊢ (F \in V \land P \in V) \to (φ \to ((X \in V \land Y \in V) \land (F \in V \land P \in V)))$
38	21 22 37	3syl	$⊢ F Walks (G) P \to (φ \to ((X \in V \land Y \in V) \land (F \in V \land P \in V)))$
39	9 38	mpcom	$⊢ φ \to ((X \in V \land Y \in V) \land (F \in V \land P \in V))$
40	7	ispthson	$⊢ ((X \in V \land Y \in V) \land (F \in V \land P \in V)) \to (F (X PathsOn (G) Y) P \leftrightarrow (F (X TrailsOn (G) Y) P \land F Paths (G) P))$
41	39 40	syl	$⊢ φ \to (F (X PathsOn (G) Y) P \leftrightarrow (F (X TrailsOn (G) Y) P \land F Paths (G) P))$
42	31 32 41	mpbir2and	$⊢ φ \to F (X PathsOn (G) Y) P$

Metamath Proof Explorer

Theorem 1pthond

Proof