Theorem 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=⟨“XY”⟩$$
	1wlkd.f	$$⊢F=⟨“J”⟩$$
	1wlkd.x	$$⊢\phi \to X\in V$$
	1wlkd.y	$$⊢\phi \to Y\in V$$
	1wlkd.l	$$⊢\left(\phi \wedge X=Y\right)\to I\left(J\right)=\left\{X\right\}$$
	1wlkd.j	$$⊢\left(\phi \wedge X\ne Y\right)\to \left\{X,Y\right\}\subseteq I\left(J\right)$$
	1wlkd.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	1wlkd.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
Assertion	1pthd	$$⊢\phi \to F\mathrm{Paths}\left(G\right)P$$

Proof

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