Description: Properties of an Eulerian path in a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 18-Feb-2021) (Proof shortened by AV, 30-Oct-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | eupths.i | |- I = ( iEdg ` G ) |
|
| upgriseupth.v | |- V = ( Vtx ` G ) |
||
| Assertion | upgreupthi | |- ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eupths.i | |- I = ( iEdg ` G ) |
|
| 2 | upgriseupth.v | |- V = ( Vtx ` G ) |
|
| 3 | 1 2 | upgriseupth | |- ( G e. UPGraph -> ( F ( EulerPaths ` G ) P <-> ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) ) |
| 4 | 3 | biimpa | |- ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) |