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

Metamath Proof Explorer

Theorem eupthistrl

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 ⊢ F EulerPaths ⁡ G P → F Trails ⁡ G P

Proof

Step Hyp Ref Expression
1 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
2 1 iseupth ⊢ F EulerPaths ⁡ G P ↔ F Trails ⁡ G P ∧ F : 0 ..^ F ⟶ onto dom ⁡ iEdg ⁡ G
3 2 simplbi ⊢ F EulerPaths ⁡ G P → F Trails ⁡ G P