Metamath Proof Explorer


Theorem trlsonwlkon

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 ‘ 𝐺 ) 𝐵 ) 𝑃 )

Proof

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 ‘ 𝐺 ) 𝐵 ) 𝑃 )