Metamath Proof Explorer
Description: An Eulerian path is a trail. (Contributed by Alexander van der Vekens, 24-Nov-2017) (Revised by AV, 18-Feb-2021)
|
|
Ref |
Expression |
|
Assertion |
eupthistrl |
⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
| 2 |
1
|
iseupth |
⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom ( iEdg ‘ 𝐺 ) ) ) |
| 3 |
2
|
simplbi |
⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) |