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 ⊢V=Vtx⁡G
Assertion pthsonprop ⊢FAPathsOn⁡GBP→G∈V∧A∈V∧B∈V∧F∈V∧P∈V∧FATrailsOn⁡GBP∧FPaths⁡GP

Proof

Step Hyp Ref Expression
1 pthsonfval.v ⊢V=Vtx⁡G
2 1 ispthson ⊢A∈V∧B∈V∧F∈V∧P∈V→FAPathsOn⁡GBP↔FATrailsOn⁡GBP∧FPaths⁡GP
3 2 3adantl1 ⊢G∈V∧A∈V∧B∈V∧F∈V∧P∈V→FAPathsOn⁡GBP↔FATrailsOn⁡GBP∧FPaths⁡GP
4 df-pthson ⊢PathsOn=g∈V⟼a∈Vtx⁡g,b∈Vtx⁡g⟼fp|faTrailsOn⁡gbp∧fPaths⁡gp
5 1 3 4 wksonproplem ⊢FAPathsOn⁡GBP→G∈V∧A∈V∧B∈V∧F∈V∧P∈V∧FATrailsOn⁡GBP∧FPaths⁡GP