Theorem pthsonfval

Description: The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017) (Revised by AV, 16-Jan-2021) (Revised by AV, 21-Mar-2021)

	Ref	Expression
Hypothesis	pthsonfval.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	pthsonfval	$$⊢\left(A\in V\wedge B\in V\right)\to A\mathrm{PathsOn}\left(G\right)B=\left\{⟨f,p⟩|\left(f\left(A\mathrm{TrailsOn}\left(G\right)B\right)p\wedge f\mathrm{Paths}\left(G\right)p\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		pthsonfval.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	1vgrex	$$⊢A\in V\to G\in \mathrm{V}$$
3	2	adantr	$$⊢\left(A\in V\wedge B\in V\right)\to G\in \mathrm{V}$$
4		simpl	$$⊢\left(A\in V\wedge B\in V\right)\to A\in V$$
5	4 1	eleqtrdi	$$⊢\left(A\in V\wedge B\in V\right)\to A\in \mathrm{Vtx}\left(G\right)$$
6		simpr	$$⊢\left(A\in V\wedge B\in V\right)\to B\in V$$
7	6 1	eleqtrdi	$$⊢\left(A\in V\wedge B\in V\right)\to B\in \mathrm{Vtx}\left(G\right)$$
8		df-pthson	$$⊢\mathrm{PathsOn}=\left(g\in \mathrm{V}⟼\left(a\in \mathrm{Vtx}\left(g\right),b\in \mathrm{Vtx}\left(g\right)⟼\left\{⟨f,p⟩|\left(f\left(a\mathrm{TrailsOn}\left(g\right)b\right)p\wedge f\mathrm{Paths}\left(g\right)p\right)\right\}\right)\right)$$
9	3 5 7 8	mptmpoopabovd	$$⊢\left(A\in V\wedge B\in V\right)\to A\mathrm{PathsOn}\left(G\right)B=\left\{⟨f,p⟩|\left(f\left(A\mathrm{TrailsOn}\left(G\right)B\right)p\wedge f\mathrm{Paths}\left(G\right)p\right)\right\}$$