Metamath Proof Explorer

Theorem istrlson

Description: Properties of a pair of functions to be a trail between two given vertices. (Contributed by Alexander van der Vekens, 3-Nov-2017) (Revised by AV, 7-Jan-2021) (Revised by AV, 21-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 trlsonfval.v ⊢ V = Vtx ⁡ G
2 1 trlsonfval ⊢ A ∈ V ∧ B ∈ V → A TrailsOn ⁡ G B = f p | f A WalksOn ⁡ G B p ∧ f Trails ⁡ G p
3 2 breqd ⊢ A ∈ V ∧ B ∈ V → F A TrailsOn ⁡ G B P ↔ F f p | f A WalksOn ⁡ G B p ∧ f Trails ⁡ G p P
4 breq12 ⊢ f = F ∧ p = P → f A WalksOn ⁡ G B p ↔ F A WalksOn ⁡ G B P
5 breq12 ⊢ f = F ∧ p = P → f Trails ⁡ G p ↔ F Trails ⁡ G P
6 4 5 anbi12d ⊢ f = F ∧ p = P → f A WalksOn ⁡ G B p ∧ f Trails ⁡ G p ↔ F A WalksOn ⁡ G B P ∧ F Trails ⁡ G P
7 eqid ⊢ f p | f A WalksOn ⁡ G B p ∧ f Trails ⁡ G p = f p | f A WalksOn ⁡ G B p ∧ f Trails ⁡ G p
8 6 7 brabga ⊢ F ∈ U ∧ P ∈ Z → F f p | f A WalksOn ⁡ G B p ∧ f Trails ⁡ G p P ↔ F A WalksOn ⁡ G B P ∧ F Trails ⁡ G P
9 3 8 sylan9bb ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ U ∧ P ∈ Z → F A TrailsOn ⁡ G B P ↔ F A WalksOn ⁡ G B P ∧ F Trails ⁡ G P