Theorem 1trld

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 trail. The two vertices need not be distinct (in the case of a loop). (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	1trld	$$⊢\phi \to F\mathrm{Trails}\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	1wlkd	$$⊢\phi \to F\mathrm{Walks}\left(G\right)P$$
10		funcnvs1	$$⊢\mathrm{Fun}{⟨“J”⟩}^{-1}$$
11	2	cnveqi	$$⊢F^{-1}={⟨“J”⟩}^{-1}$$
12	11	funeqi	$$⊢\mathrm{Fun}{F}^{-1}\leftrightarrow \mathrm{Fun}{⟨“J”⟩}^{-1}$$
13	10 12	mpbir	$$⊢\mathrm{Fun}{F}^{-1}$$
14		istrl	$$⊢F\mathrm{Trails}\left(G\right)P\leftrightarrow \left(F\mathrm{Walks}\left(G\right)P\wedge \mathrm{Fun}{F}^{-1}\right)$$
15	9 13 14	sylanblrc	$$⊢\phi \to F\mathrm{Trails}\left(G\right)P$$