Theorem 1wlkd

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 walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021) (Revised by AV, 23-Mar-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	1wlkd	$$⊢\phi \to F\mathrm{Walks}\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	1wlkdlem3	$$⊢\phi \to F\in \mathrm{Word}\mathrm{dom}I$$
10	1 2 3 4	1wlkdlem1	$$⊢\phi \to P:\left(0\dots \left|F\right|\right)⟶V$$
11	1 2 3 4 5 6	1wlkdlem4	$$⊢\phi \to \forall k\in \left(0..^\left|F\right|\right)if-\left(P\left(k\right)=P\left(k+1\right),I\left(F\left(k\right)\right)=\left\{P\left(k\right)\right\},\left\{P\left(k\right),P\left(k+1\right)\right\}\subseteq I\left(F\left(k\right)\right)\right)$$
12	7	1vgrex	$$⊢X\in V\to G\in \mathrm{V}$$
13	7 8	iswlkg	$$⊢G\in \mathrm{V}\to \left(F\mathrm{Walks}\left(G\right)P\leftrightarrow \left(F\in \mathrm{Word}\mathrm{dom}I\wedge P:\left(0\dots \left|F\right|\right)⟶V\wedge \forall k\in \left(0..^\left|F\right|\right)if-\left(P\left(k\right)=P\left(k+1\right),I\left(F\left(k\right)\right)=\left\{P\left(k\right)\right\},\left\{P\left(k\right),P\left(k+1\right)\right\}\subseteq I\left(F\left(k\right)\right)\right)\right)\right)$$
14	3 12 13	3syl	$$⊢\phi \to \left(F\mathrm{Walks}\left(G\right)P\leftrightarrow \left(F\in \mathrm{Word}\mathrm{dom}I\wedge P:\left(0\dots \left|F\right|\right)⟶V\wedge \forall k\in \left(0..^\left|F\right|\right)if-\left(P\left(k\right)=P\left(k+1\right),I\left(F\left(k\right)\right)=\left\{P\left(k\right)\right\},\left\{P\left(k\right),P\left(k+1\right)\right\}\subseteq I\left(F\left(k\right)\right)\right)\right)\right)$$
15	9 10 11 14	mpbir3and	$$⊢\phi \to F\mathrm{Walks}\left(G\right)P$$