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 ) } ) )