Definition df-trlson 26590

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

Assertion

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

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

Detailed syntax breakdown of Definition df-trlson

Step	Hyp	Ref	Expression
1		ctrlson 26588	. 2 class TrailsOn
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		cwlkson 26493	. . . . . . . . 9 class WalksOn
16	6, 15	cfv 5888	. . . . . . . 8 class (WalksOn ` g )
17	13, 14, 16	co 6650	. . . . . . 7 class ( a (WalksOn ` g ) b )
18	10, 12, 17	wbr 4653	. . . . . 6 wff f ( a (WalksOn ` g ) b ) p
19		ctrls 26587	. . . . . . . 8 class Trails
20	6, 19	cfv 5888	. . . . . . 7 class (Trails ` g )
21	10, 12, 20	wbr 4653	. . . . . 6 wff f (Trails ` g ) p
22	18, 21	wa 384	. . . . 5 wff ( f ( a (WalksOn ` g ) b ) p /\ f (Trails ` g ) p )
23	22, 9, 11	copab 4712	. . . 4 class { <. f , p >. | ( f ( a (WalksOn ` g ) b ) p /\ f (Trails ` g ) p ) }
24	4, 5, 8, 8, 23	cmpt2 6652	. . 3 class ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f ( a (WalksOn ` g ) b ) p /\ f (Trails ` 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 (WalksOn ` g ) b ) p /\ f (Trails ` g ) p ) } ) )
26	1, 25	wceq 1483	1 wff TrailsOn = ( g e. _V |-> ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f ( a (WalksOn ` g ) b ) p /\ f (Trails ` g ) p ) } ) )

This definition is referenced by:  trlsonfval  26602  trlsonprop  26604