Metamath Proof Explorer


Theorem spthsfval

Description: The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017) (Revised by AV, 9-Jan-2021) (Revised by AV, 29-Oct-2021)

Ref Expression
Assertion spthsfval
|- ( SPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' p ) }

Proof

Step Hyp Ref Expression
1 biidd
 |-  ( g = G -> ( Fun `' p <-> Fun `' p ) )
2 df-spths
 |-  SPaths = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ Fun `' p ) } )
3 1 2 fvmptopab
 |-  ( SPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' p ) }