Metamath Proof Explorer

Definition df-eupth

Description: Define the set of all Eulerian paths on an arbitrary graph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 18-Feb-2021)

Ref Expression
Assertion df-eupth 
|- EulerPaths = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ceupth 
 |-  EulerPaths
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vf 
 |-  f
4 vp 
 |-  p
5 3 cv 
 |-  f
6 ctrls 
 |-  Trails
7 1 cv 
 |-  g
8 7 6 cfv 
 |-  ( Trails ` g )
9 4 cv 
 |-  p
10 5 9 8 wbr 
 |-  f ( Trails ` g ) p
11 cc0 
 |-  0
12 cfzo 
 |-  ..^
13 chash 
 |-  #
14 5 13 cfv 
 |-  ( # ` f )
15 11 14 12 co 
 |-  ( 0 ..^ ( # ` f ) )
16 ciedg 
 |-  iEdg
17 7 16 cfv 
 |-  ( iEdg ` g )
18 17 cdm 
 |-  dom ( iEdg ` g )
19 15 18 5 wfo 
 |-  f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g )
20 10 19 wa 
 |-  ( f ( Trails ` g ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g ) )
21 20 3 4 copab 
 |-  { <. f , p >. | ( f ( Trails ` g ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g ) ) }
22 1 2 21 cmpt 
 |-  ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g ) ) } )
23 0 22 wceq 
 |-  EulerPaths = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g ) ) } )