Definition df-spths

Description: Define the set of all simple paths (in an undirected graph).

According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory) , 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices."

Therefore, a simple path can be represented by an injective mapping f from { 1 , ... , n } and an injective mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the simple path is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 9-Jan-2021)

	Ref	Expression
Assertion	df-spths	$$⊢\mathrm{SPaths}=\left(g\in \mathrm{V}⟼\left\{⟨f,p⟩|\left(f\mathrm{Trails}\left(g\right)p\wedge \mathrm{Fun}{p}^{-1}\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cspths	$$class\mathrm{SPaths}$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4		vp	$$setvarp$$
5	3	cv	$$setvarf$$
6		ctrls	$$class\mathrm{Trails}$$
7	1	cv	$$setvarg$$
8	7 6	cfv	$$class\mathrm{Trails}\left(g\right)$$
9	4	cv	$$setvarp$$
10	5 9 8	wbr	$$wfff\mathrm{Trails}\left(g\right)p$$
11	9	ccnv	$$class{p}^{-1}$$
12	11	wfun	$$wff\mathrm{Fun}{p}^{-1}$$
13	10 12	wa	$$wff\left(f\mathrm{Trails}\left(g\right)p\wedge \mathrm{Fun}{p}^{-1}\right)$$
14	13 3 4	copab	$$class\left\{⟨f,p⟩|\left(f\mathrm{Trails}\left(g\right)p\wedge \mathrm{Fun}{p}^{-1}\right)\right\}$$
15	1 2 14	cmpt	$$class\left(g\in \mathrm{V}⟼\left\{⟨f,p⟩|\left(f\mathrm{Trails}\left(g\right)p\wedge \mathrm{Fun}{p}^{-1}\right)\right\}\right)$$
16	0 15	wceq	$$wff\mathrm{SPaths}=\left(g\in \mathrm{V}⟼\left\{⟨f,p⟩|\left(f\mathrm{Trails}\left(g\right)p\wedge \mathrm{Fun}{p}^{-1}\right)\right\}\right)$$