Metamath Proof Explorer

Theorem ispthson

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

Ref Expression
Hypothesis pthsonfval.v ⊢ V = Vtx ⁡ G
Assertion ispthson ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ U ∧ P ∈ Z → F A PathsOn ⁡ G B P ↔ F A TrailsOn ⁡ G B P ∧ F Paths ⁡ G P

Proof

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