Theorem upgr1pthond

Description: In a pseudograph 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 AV, 22-Jan-2021)

	Ref	Expression
Hypotheses	upgr1wlkd.p	$$⊢P=⟨“XY”⟩$$
	upgr1wlkd.f	$$⊢F=⟨“J”⟩$$
	upgr1wlkd.x	$$⊢\phi \to X\in \mathrm{Vtx}\left(G\right)$$
	upgr1wlkd.y	$$⊢\phi \to Y\in \mathrm{Vtx}\left(G\right)$$
	upgr1wlkd.j	$$⊢\phi \to \mathrm{iEdg}\left(G\right)\left(J\right)=\left\{X,Y\right\}$$
	upgr1wlkd.g	$$⊢\phi \to G\in \mathrm{UPGraph}$$
Assertion	upgr1pthond	$$⊢\phi \to F\left(X\mathrm{PathsOn}\left(G\right)Y\right)P$$

Proof

Step	Hyp	Ref	Expression
1		upgr1wlkd.p	$$⊢P=⟨“XY”⟩$$
2		upgr1wlkd.f	$$⊢F=⟨“J”⟩$$
3		upgr1wlkd.x	$$⊢\phi \to X\in \mathrm{Vtx}\left(G\right)$$
4		upgr1wlkd.y	$$⊢\phi \to Y\in \mathrm{Vtx}\left(G\right)$$
5		upgr1wlkd.j	$$⊢\phi \to \mathrm{iEdg}\left(G\right)\left(J\right)=\left\{X,Y\right\}$$
6		upgr1wlkd.g	$$⊢\phi \to G\in \mathrm{UPGraph}$$
7	1 2 3 4 5	upgr1wlkdlem1	$$⊢\left(\phi \wedge X=Y\right)\to \mathrm{iEdg}\left(G\right)\left(J\right)=\left\{X\right\}$$
8	1 2 3 4 5	upgr1wlkdlem2	$$⊢\left(\phi \wedge X\ne Y\right)\to \left\{X,Y\right\}\subseteq \mathrm{iEdg}\left(G\right)\left(J\right)$$
9		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
10		eqid	$$⊢\mathrm{iEdg}\left(G\right)=\mathrm{iEdg}\left(G\right)$$
11	1 2 3 4 7 8 9 10	1pthond	$$⊢\phi \to F\left(X\mathrm{PathsOn}\left(G\right)Y\right)P$$