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 6 adantl 
 |-  ( ( T. /\ g = G ) -> ( f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g ) <-> f : ( 0 ..^ ( # ` f ) ) -onto-> dom I ) )
8 wksv 
 |-  { <. f , p >. | f ( Walks ` G ) p } e. _V
9 trliswlk 
 |-  ( f ( Trails ` G ) p -> f ( Walks ` G ) p )
10 9 ssopab2i 
 |-  { <. f , p >. | f ( Trails ` G ) p } C_ { <. f , p >. | f ( Walks ` G ) p }
11 8 10 ssexi 
 |-  { <. f , p >. | f ( Trails ` G ) p } e. _V
12 11 a1i 
 |-  ( T. -> { <. f , p >. | f ( Trails ` G ) p } e. _V )
13 df-eupth 
 |-  EulerPaths = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g ) ) } )
14 7 12 13 fvmptopab 
 |-  ( T. -> ( EulerPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom I ) } )
15 14 mptru 
 |-  ( EulerPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom I ) }