Description: A trail between two vertices is a walk between these vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017) (Revised by AV, 7-Jan-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | trlsonwlkon | ⊢ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) | |
| 2 | 1 | trlsonprop | ⊢ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) ) |
| 3 | simp3l | ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) → 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ) | |
| 4 | 2 3 | syl | ⊢ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ) |