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