Metamath Proof Explorer


Theorem pthsonprop

Description: Properties of a path between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017) (Revised by AV, 16-Jan-2021)

Ref Expression
Hypothesis pthsonfval.v 𝑉 = ( Vtx ‘ 𝐺 )
Assertion pthsonprop ( 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 pthsonfval.v 𝑉 = ( Vtx ‘ 𝐺 )
2 1 ispthson ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) )
3 2 3adantl1 ( ( ( 𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) )
4 df-pthson PathsOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝𝑓 ( Paths ‘ 𝑔 ) 𝑝 ) } ) )
5 pthiswlk ( 𝑓 ( Paths ‘ 𝐺 ) 𝑝𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
6 5 adantl ( ( ( 𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉 ) ∧ 𝑓 ( Paths ‘ 𝐺 ) 𝑝 ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
7 1 3 4 6 wksonproplem ( 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) )