Metamath Proof Explorer


Definition df-trlson

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)

Ref Expression
Assertion 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 ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctrlson
 |-  TrailsOn
1 vg
 |-  g
2 cvv
 |-  _V
3 va
 |-  a
4 cvtx
 |-  Vtx
5 1 cv
 |-  g
6 5 4 cfv
 |-  ( Vtx ` g )
7 vb
 |-  b
8 vf
 |-  f
9 vp
 |-  p
10 8 cv
 |-  f
11 3 cv
 |-  a
12 cwlkson
 |-  WalksOn
13 5 12 cfv
 |-  ( WalksOn ` g )
14 7 cv
 |-  b
15 11 14 13 co
 |-  ( a ( WalksOn ` g ) b )
16 9 cv
 |-  p
17 10 16 15 wbr
 |-  f ( a ( WalksOn ` g ) b ) p
18 ctrls
 |-  Trails
19 5 18 cfv
 |-  ( Trails ` g )
20 10 16 19 wbr
 |-  f ( Trails ` g ) p
21 17 20 wa
 |-  ( f ( a ( WalksOn ` g ) b ) p /\ f ( Trails ` g ) p )
22 21 8 9 copab
 |-  { <. f , p >. | ( f ( a ( WalksOn ` g ) b ) p /\ f ( Trails ` g ) p ) }
23 3 7 6 6 22 cmpo
 |-  ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( a ( WalksOn ` g ) b ) p /\ f ( Trails ` g ) p ) } )
24 1 2 23 cmpt
 |-  ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( a ( WalksOn ` g ) b ) p /\ f ( Trails ` g ) p ) } ) )
25 0 24 wceq
 |-  TrailsOn = ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( a ( WalksOn ` g ) b ) p /\ f ( Trails ` g ) p ) } ) )