Metamath Proof Explorer

Theorem isspthson

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

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

Proof

Step Hyp Ref Expression
1 pthsonfval.v ⊢ V = Vtx ⁡ G
2 1 spthson ⊢ A ∈ V ∧ B ∈ V → A SPathsOn ⁡ G B = f p | f A TrailsOn ⁡ G B p ∧ f SPaths ⁡ G p
3 2 breqd ⊢ A ∈ V ∧ B ∈ V → F A SPathsOn ⁡ G B P ↔ F f p | f A TrailsOn ⁡ G B p ∧ f SPaths ⁡ 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 SPaths ⁡ G p ↔ F SPaths ⁡ G P
6 4 5 anbi12d ⊢ f = F ∧ p = P → f A TrailsOn ⁡ G B p ∧ f SPaths ⁡ G p ↔ F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P
7 eqid ⊢ f p | f A TrailsOn ⁡ G B p ∧ f SPaths ⁡ G p = f p | f A TrailsOn ⁡ G B p ∧ f SPaths ⁡ G p
8 6 7 brabga ⊢ F ∈ U ∧ P ∈ Z → F f p | f A TrailsOn ⁡ G B p ∧ f SPaths ⁡ G p P ↔ F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P
9 3 8 sylan9bb ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ U ∧ P ∈ Z → F A SPathsOn ⁡ G B P ↔ F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P