Metamath Proof Explorer


Theorem 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 wksv f p | f Walks G p V
9 8 a1i A V B V f p | f Walks G p V
10 spthiswlk f SPaths G p f Walks G p
11 10 adantl A V B V f SPaths G p f Walks G p
12 df-spthson SPathsOn = g V a Vtx g , b Vtx g f p | f a TrailsOn g b p f SPaths g p
13 3 5 7 9 11 12 mptmpoopabovd A V B V A SPathsOn G B = f p | f A TrailsOn G B p f SPaths G p