Definition df-pths

Description: Define the set of all 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."

According to Bollobas: "... a path is a walk with distinct vertices.", see Notation of Bollobas p. 5. (A walk with distinct vertices is actually a simple path, see upgrwlkdvspth ).

Therefore, a path can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, which is injective restricted to the set { 1 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the 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 and Mario Carneiro, 4-Oct-2017) (Revised by AV, 9-Jan-2021)

	Ref	Expression
Assertion	df-pths	$$⊢\mathrm{Paths}=\left(g\in \mathrm{V}⟼\left\{⟨f,p⟩|\left(f\mathrm{Trails}\left(g\right)p\wedge \mathrm{Fun}{\left({p\upharpoonright }_{\left(1..^\left|f\right|\right)}\right)}^{-1}\wedge p\left[\left\{0,\left|f\right|\right\}\right]\cap p\left[\left(1..^\left|f\right|\right)\right]=\varnothing \right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpths	$$class\mathrm{Paths}$$
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		c1	$$class1$$
12		cfzo	$$class..^$$
13		chash	$$class\left|.\right|$$
14	5 13	cfv	$$class\left|f\right|$$
15	11 14 12	co	$$class\left(1..^\left|f\right|\right)$$
16	9 15	cres	$$class\left({p\upharpoonright }_{\left(1..^\left|f\right|\right)}\right)$$
17	16	ccnv	$$class{\left({p\upharpoonright }_{\left(1..^\left|f\right|\right)}\right)}^{-1}$$
18	17	wfun	$$wff\mathrm{Fun}{\left({p\upharpoonright }_{\left(1..^\left|f\right|\right)}\right)}^{-1}$$
19		cc0	$$class0$$
20	19 14	cpr	$$class\left\{0,\left|f\right|\right\}$$
21	9 20	cima	$$classp\left[\left\{0,\left|f\right|\right\}\right]$$
22	9 15	cima	$$classp\left[\left(1..^\left|f\right|\right)\right]$$
23	21 22	cin	$$class\left(p\left[\left\{0,\left|f\right|\right\}\right]\cap p\left[\left(1..^\left|f\right|\right)\right]\right)$$
24		c0	$$class\varnothing$$
25	23 24	wceq	$$wffp\left[\left\{0,\left|f\right|\right\}\right]\cap p\left[\left(1..^\left|f\right|\right)\right]=\varnothing$$
26	10 18 25	w3a	$$wff\left(f\mathrm{Trails}\left(g\right)p\wedge \mathrm{Fun}{\left({p\upharpoonright }_{\left(1..^\left|f\right|\right)}\right)}^{-1}\wedge p\left[\left\{0,\left|f\right|\right\}\right]\cap p\left[\left(1..^\left|f\right|\right)\right]=\varnothing \right)$$
27	26 3 4	copab	$$class\left\{⟨f,p⟩|\left(f\mathrm{Trails}\left(g\right)p\wedge \mathrm{Fun}{\left({p\upharpoonright }_{\left(1..^\left|f\right|\right)}\right)}^{-1}\wedge p\left[\left\{0,\left|f\right|\right\}\right]\cap p\left[\left(1..^\left|f\right|\right)\right]=\varnothing \right)\right\}$$
28	1 2 27	cmpt	$$class\left(g\in \mathrm{V}⟼\left\{⟨f,p⟩|\left(f\mathrm{Trails}\left(g\right)p\wedge \mathrm{Fun}{\left({p\upharpoonright }_{\left(1..^\left|f\right|\right)}\right)}^{-1}\wedge p\left[\left\{0,\left|f\right|\right\}\right]\cap p\left[\left(1..^\left|f\right|\right)\right]=\varnothing \right)\right\}\right)$$
29	0 28	wceq	$$wff\mathrm{Paths}=\left(g\in \mathrm{V}⟼\left\{⟨f,p⟩|\left(f\mathrm{Trails}\left(g\right)p\wedge \mathrm{Fun}{\left({p\upharpoonright }_{\left(1..^\left|f\right|\right)}\right)}^{-1}\wedge p\left[\left\{0,\left|f\right|\right\}\right]\cap p\left[\left(1..^\left|f\right|\right)\right]=\varnothing \right)\right\}\right)$$