Metamath Proof Explorer


Definition df-spthson

Description: Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 9-Jan-2021)

Ref Expression
Assertion df-spthson SPathsOn = g V a Vtx g , b Vtx g f p | f a TrailsOn g b p f SPaths g p

Detailed syntax breakdown

Step Hyp Ref Expression
0 cspthson class SPathsOn
1 vg setvar g
2 cvv class V
3 va setvar a
4 cvtx class Vtx
5 1 cv setvar g
6 5 4 cfv class Vtx g
7 vb setvar b
8 vf setvar f
9 vp setvar p
10 8 cv setvar f
11 3 cv setvar a
12 ctrlson class TrailsOn
13 5 12 cfv class TrailsOn g
14 7 cv setvar b
15 11 14 13 co class a TrailsOn g b
16 9 cv setvar p
17 10 16 15 wbr wff f a TrailsOn g b p
18 cspths class SPaths
19 5 18 cfv class SPaths g
20 10 16 19 wbr wff f SPaths g p
21 17 20 wa wff f a TrailsOn g b p f SPaths g p
22 21 8 9 copab class f p | f a TrailsOn g b p f SPaths g p
23 3 7 6 6 22 cmpo class a Vtx g , b Vtx g f p | f a TrailsOn g b p f SPaths g p
24 1 2 23 cmpt class g V a Vtx g , b Vtx g f p | f a TrailsOn g b p f SPaths g p
25 0 24 wceq wff SPathsOn = g V a Vtx g , b Vtx g f p | f a TrailsOn g b p f SPaths g p