Theorem spthonprop

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

	Ref	Expression
Hypothesis	pthsonfval.v	|- V = ( Vtx ` G )
Assertion	spthonprop	|- ( F ( A ( SPathsOn ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) ) )

Proof

Step	Hyp	Ref	Expression
1		pthsonfval.v	|- V = ( Vtx ` G )
2	1	isspthson	|- ( ( ( A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) ) )
3	2	3adantl1	|- ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) ) )
4		df-spthson	|- SPathsOn = ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( a ( TrailsOn ` g ) b ) p /\ f ( SPaths ` g ) p ) } ) )
5	1 3 4	wksonproplem	|- ( F ( A ( SPathsOn ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) ) )