This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eupths

Description: The Eulerian paths on the graph G . (Contributed by AV, 18-Feb-2021) (Revised by AV, 29-Oct-2021)

Ref Expression
Hypothesis eupths.i 
|- I = ( iEdg ` G )
Assertion eupths 
|- ( EulerPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom I ) }

Proof

Step Hyp Ref Expression
1 eupths.i 
 |-  I = ( iEdg ` G )
2 fveq2 
 |-  ( g = G -> ( iEdg ` g ) = ( iEdg ` G ) )
3 2 1 eqtr4di 
 |-  ( g = G -> ( iEdg ` g ) = I )
4 3 dmeqd 
 |-  ( g = G -> dom ( iEdg ` g ) = dom I )
5 foeq3 
 |-  ( dom ( iEdg ` g ) = dom I -> ( f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g ) <-> f : ( 0 ..^ ( # ` f ) ) -onto-> dom I ) )
6 4 5 syl 
 |-  ( g = G -> ( f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g ) <-> f : ( 0 ..^ ( # ` f ) ) -onto-> dom I ) )
7 df-eupth 
 |-  EulerPaths = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g ) ) } )
8 6 7 fvmptopab 
 |-  ( EulerPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom I ) }