Definition df-trls

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

According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory) , 3-Oct-2017): "A trail is a walk in which all edges are distinct.

According to Bollobas: "... walk is called a trail if all its edges are distinct.", see Definition of Bollobas p. 5.

Therefore, a trail can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the trail 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, 28-Dec-2020)

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

Detailed syntax breakdown

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