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

Metamath Proof Explorer

Theorem spthdifv

Description: The vertices of a simple path are distinct, so the vertex function is one-to-one. (Contributed by Alexander van der Vekens, 26-Jan-2018) (Revised by AV, 5-Jun-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion spthdifv ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 isspth ⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) )
2 trliswlk ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
3 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4 3 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
5 df-f1 ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) ↔ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ◡ 𝑃 ) )
6 5 simplbi2 ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( Fun ◡ 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) ) )
7 2 4 6 3syl ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( Fun ◡ 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) ) )
8 7 imp ⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) )
9 1 8 sylbi ⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) )