This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Walks, paths and cycles Paths and simple paths spthson
Description: The set of simple paths between two vertices (in an undirected graph).
(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
spthson ⊢ A ∈ V ∧ B ∈ V → A SPathsOn G B = f p | f A TrailsOn G B p ∧ f SPaths G p
Proof
Step
Hyp
Ref
Expression
1
pthsonfval.v ⊢ V = Vtx G
2
1
1vgrex ⊢ A ∈ V → G ∈ V
3
2
adantr ⊢ A ∈ V ∧ B ∈ V → G ∈ V
4
simpl ⊢ A ∈ V ∧ B ∈ V → A ∈ V
5
4 1
eleqtrdi ⊢ A ∈ V ∧ B ∈ V → A ∈ Vtx G
6
simpr ⊢ A ∈ V ∧ B ∈ V → B ∈ V
7
6 1
eleqtrdi ⊢ A ∈ V ∧ B ∈ V → B ∈ Vtx G
8
df-spthson ⊢ SPathsOn = g ∈ V ⟼ a ∈ Vtx g , b ∈ Vtx g ⟼ f p | f a TrailsOn g b p ∧ f SPaths g p
9
3 5 7 8
mptmpoopabovd ⊢ A ∈ V ∧ B ∈ V → A SPathsOn G B = f p | f A TrailsOn G B p ∧ f SPaths G p