Metamath Proof Explorer

Definition df-pthson

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)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpthson 
 |-  PathsOn
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 ctrlson 
 |-  TrailsOn
13 5 12 cfv 
 |-  ( TrailsOn ` g )
14 7 cv 
 |-  b
15 11 14 13 co 
 |-  ( a ( TrailsOn ` g ) b )
16 9 cv 
 |-  p
17 10 16 15 wbr 
 |-  f ( a ( TrailsOn ` g ) b ) p
18 cpths 
 |-  Paths
19 5 18 cfv 
 |-  ( Paths ` g )
20 10 16 19 wbr 
 |-  f ( Paths ` g ) p
21 17 20 wa 
 |-  ( f ( a ( TrailsOn ` g ) b ) p /\ f ( Paths ` g ) p )
22 21 8 9 copab 
 |-  { <. f , p >. | ( f ( a ( TrailsOn ` g ) b ) p /\ f ( Paths ` g ) p ) }
23 3 7 6 6 22 cmpo 
 |-  ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( a ( TrailsOn ` g ) b ) p /\ f ( Paths ` g ) p ) } )
24 1 2 23 cmpt 
 |-  ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( a ( TrailsOn ` g ) b ) p /\ f ( Paths ` g ) p ) } ) )
25 0 24 wceq 
 |-  PathsOn = ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( a ( TrailsOn ` g ) b ) p /\ f ( Paths ` g ) p ) } ) )