Definition df-pthson 26614

Description: Define the collection of paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.)

Assertion

Ref	Expression
df-pthson	|- PathsOn = ( g e. _V |-> ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f ( a (TrailsOn ` g ) b ) p /\ f (Paths ` g ) p ) } ) )

Distinct variable groups:   f, g, p   a, b, g, f, p

Detailed syntax breakdown of Definition df-pthson

Step	Hyp	Ref	Expression
1		cpthson 26610	. 2 class PathsOn
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		va	. . . 4 setvar a
5		vb	. . . 4 setvar b
6	2	cv 1482	. . . . 5 class g
7		cvtx 25874	. . . . 5 class Vtx
8	6, 7	cfv 5888	. . . 4 class (Vtx ` g )
9		vf	. . . . . . . 8 setvar f
10	9	cv 1482	. . . . . . 7 class f
11		vp	. . . . . . . 8 setvar p
12	11	cv 1482	. . . . . . 7 class p
13	4	cv 1482	. . . . . . . 8 class a
14	5	cv 1482	. . . . . . . 8 class b
15		ctrlson 26588	. . . . . . . . 9 class TrailsOn
16	6, 15	cfv 5888	. . . . . . . 8 class (TrailsOn ` g )
17	13, 14, 16	co 6650	. . . . . . 7 class ( a (TrailsOn ` g ) b )
18	10, 12, 17	wbr 4653	. . . . . 6 wff f ( a (TrailsOn ` g ) b ) p
19		cpths 26608	. . . . . . . 8 class Paths
20	6, 19	cfv 5888	. . . . . . 7 class (Paths ` g )
21	10, 12, 20	wbr 4653	. . . . . 6 wff f (Paths ` g ) p
22	18, 21	wa 384	. . . . 5 wff ( f ( a (TrailsOn ` g ) b ) p /\ f (Paths ` g ) p )
23	22, 9, 11	copab 4712	. . . 4 class { <. f , p >. | ( f ( a (TrailsOn ` g ) b ) p /\ f (Paths ` g ) p ) }
24	4, 5, 8, 8, 23	cmpt2 6652	. . 3 class ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f ( a (TrailsOn ` g ) b ) p /\ f (Paths ` g ) p ) } )
25	2, 3, 24	cmpt 4729	. 2 class ( g e. _V |-> ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f ( a (TrailsOn ` g ) b ) p /\ f (Paths ` g ) p ) } ) )
26	1, 25	wceq 1483	1 wff PathsOn = ( g e. _V |-> ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f ( a (TrailsOn ` g ) b ) p /\ f (Paths ` g ) p ) } ) )

This definition is referenced by:  pthsonfval  26636  pthsonprop  26640