Metamath Proof Explorer


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 Paths=gVfp|fTrailsgpFunp1..^f-1p0fp1..^f=

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpths classPaths
1 vg setvarg
2 cvv classV
3 vf setvarf
4 vp setvarp
5 3 cv setvarf
6 ctrls classTrails
7 1 cv setvarg
8 7 6 cfv classTrailsg
9 4 cv setvarp
10 5 9 8 wbr wfffTrailsgp
11 c1 class1
12 cfzo class..^
13 chash class.
14 5 13 cfv classf
15 11 14 12 co class1..^f
16 9 15 cres classp1..^f
17 16 ccnv classp1..^f-1
18 17 wfun wffFunp1..^f-1
19 cc0 class0
20 19 14 cpr class0f
21 9 20 cima classp0f
22 9 15 cima classp1..^f
23 21 22 cin classp0fp1..^f
24 c0 class
25 23 24 wceq wffp0fp1..^f=
26 10 18 25 w3a wfffTrailsgpFunp1..^f-1p0fp1..^f=
27 26 3 4 copab classfp|fTrailsgpFunp1..^f-1p0fp1..^f=
28 1 2 27 cmpt classgVfp|fTrailsgpFunp1..^f-1p0fp1..^f=
29 0 28 wceq wffPaths=gVfp|fTrailsgpFunp1..^f-1p0fp1..^f=