Metamath Proof Explorer

Theorem trlsonprop

Description: Properties of a trail between two vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017) (Revised by AV, 7-Jan-2021) (Proof shortened by AV, 16-Jan-2021)

Ref Expression
Hypothesis trlsonfval.v ⊢ V = Vtx ⁡ G
Assertion trlsonprop ⊢ F A TrailsOn ⁡ G B P → G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ∧ F A WalksOn ⁡ G B P ∧ F Trails ⁡ G P

Proof

Step Hyp Ref Expression
1 trlsonfval.v ⊢ V = Vtx ⁡ G
2 1 istrlson ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V → F A TrailsOn ⁡ G B P ↔ F A WalksOn ⁡ G B P ∧ F Trails ⁡ G P
3 2 3adantl1 ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V → F A TrailsOn ⁡ G B P ↔ F A WalksOn ⁡ G B P ∧ F Trails ⁡ G P
4 df-trlson ⊢ TrailsOn = g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a WalksOn ⁡ g b p ∧ f Trails ⁡ g p
5 trliswlk ⊢ f Trails ⁡ G p → f Walks ⁡ G p
6 5 adantl ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ f Trails ⁡ G p → f Walks ⁡ G p
7 1 3 4 6 wksonproplem ⊢ F A TrailsOn ⁡ G B P → G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ∧ F A WalksOn ⁡ G B P ∧ F Trails ⁡ G P