Metamath Proof Explorer

Definition df-spthson

Description: Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 9-Jan-2021)

Ref Expression
Assertion df-spthson 
|- SPathsOn = ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( a ( TrailsOn ` g ) b ) p /\ f ( SPaths ` g ) p ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cspthson 
 |-  SPathsOn
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 cspths 
 |-  SPaths
19 5 18 cfv 
 |-  ( SPaths ` g )
20 10 16 19 wbr 
 |-  f ( SPaths ` g ) p
21 17 20 wa 
 |-  ( f ( a ( TrailsOn ` g ) b ) p /\ f ( SPaths ` g ) p )
22 21 8 9 copab 
 |-  { <. f , p >. | ( f ( a ( TrailsOn ` g ) b ) p /\ f ( SPaths ` 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 ( SPaths ` 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 ( SPaths ` g ) p ) } ) )
25 0 24 wceq 
 |-  SPathsOn = ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( a ( TrailsOn ` g ) b ) p /\ f ( SPaths ` g ) p ) } ) )