This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Eulerian paths and the Konigsberg Bridge problem Eulerian paths eupthpf
Description: The P function in an Eulerian path is a function from a finite
sequence of nonnegative integers to the vertices. (Contributed by Mario
Carneiro , 12-Mar-2015) (Revised by AV , 18-Feb-2021)
Ref
Expression
Assertion
eupthpf ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
Proof
Step
Hyp
Ref
Expression
1
eupthiswlk ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
2
eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3
2
wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
4
1 3
syl ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )